The
notion of
logical
inference is of fundamental importance not only in all forms of
argumentation (be it formal or informal) but also in several aspects of
computing. The study of logical inference for applications requires the
understanding of combinations of logical mechanisms in several guises.
This
project is focused on specific methods for combining logics and their
semantical, algebraic and computational aspects of the resulting
combined systems. From the point of view of efficient applications,
approximating propositional and quantified inferences is a promising
approach in the taming of the intrinsic complexities involved.
Intimately related to the quest for efficiency, quantum logics and
quantum computation arise as an important research area.
The
formidable speedup of technology requires multidisciplinary researchers
involved in the hard task of providing efficient alternatives to
traditional methods of inference. To cope with this challenge, the
project involves 22 researchers with different backgrounds from USP and
UNICAMP with the support of 8 researchers from three international
research institutions.
Problem Description
A project about logical consequence can have a very wide
range. Our
project has a narrower scope, focusing on the fundaments of
combination of logics and its practical applications.
The universe of logical
combinations allows us to tackle many subjects
present in the state-of-the-art research in Logic. First, we have to
face the study of methods for combining logics. One the one hand,
logics can be put together to generate more complex systems; on the
other hane, a logic can be decomposed into simpler ones. The
combination processes can vary and generate a single logic, as in the
possible-translations approach, or the process can be asymptotic and
generate a class of logics, as in the families of logics that
approximate classical logic.
Second, there are particular
instances of logical combination that are
of interest, such as it occurs in the study of propositional
second-order intuitionistic logic, which combines features of
propositional logic, intuitionistic logic and second-order
quantification.
Third, the practical
applications of combinations of logics unfolds
into the fields of theorem proving, AI, belief revision and in the
study of novel models of computation, such as quantum computation and
quantum algorithms.
To cover this wide spectrum, we
face the problem of combining logics
from the mathematical, computational and conceptual points of view.
Objectives
The aims of this project are the study of the following
aspects of
combination of logics.
- To study the fundamental
issues of combining logics, which covers the following points:
- Specific methods for
combining logics, such as fusion, products
and fibring.
- Algebraic and categorial
aspects of logic combinations, such as Blok-Pigozzi
algebraization.
- Formal semantics for
logic combination, such as possible-translations
semantics
and society
semantics.
- The study of computational
aspects of logical combination, addressing the following topics:
- Approximations of
classical logic and the development of approximate theorem provers.
- Belief Revision and its
relation with the notions of relevance generated by approximation
processes.
- Logics with
uncertainty, as opposed to logics that reason about
uncertainty. These logics of practical interest can be modelled as a
combination of classical logics with probability theory or with fuzzy
logics.
- The study of particular
logics of interest resulting from combination of logics, namely:
- Quantum Logics, which
are connected to non-trivial mathematical questions on Hilbert Spaces,
Lie Algebras and Topology.
- Quantum algorithms
which, from the standpoint of combination mechanisms, can be seen as
superpositions of classical models.
Human Resources and Research
Strategy
The notions of logical inference and of combinations of
inference
mechanisms which are the basis of the present project call for
essential multidisciplinarity. This justifies the participation of main
researchers from different backgrounds such as Philosophy, Computer
Science and Mathematics. The institutions involved in this research
project are: the Centre for Logic, Epistemology and the History of
Science (CLE-UNICAMP), the Department of Philosophy (IFCH-UNICAMP),
the Department of Computer Science (DCC-IME-USP), the Department of
Mathematics (MAT-IME-USP) and the Department of Mathematics of the
Faculty of Sciences (MAT-UNESP-Bauru).
This congregating project
involves research in the range from
foundational and conceptual aspects of the notion of inference, with
obvious interest for philosophical argumentation, to high impact
technological aspects. There is an urgent need in Brazil of attention
to non-conventional computational technologies, with its connections
to nano-scale miniaturisation technologies and bio-molecular
computation. Although we do not directly treat these latter aspects
here, there are certainly other FAPESP sponsored projects that would
benefit from cross contacts with the resources that will be obtained
as output of the current project.
The group of researchers
consists of the following people:
- Project
Coordinator
- Walter Carnielli (IFCH
and CLE - UNICAMP)
- Task
Coordinators
- Marcelo Coniglio (IFCH
and CLE - UNICAMP)
- Marcelo Finger
(DCC-IME-USP)
- Researchers
- Angela Weiss
(MAT-IME-USP)
- Flávio Soares
Corrêa da Silva (DCC-IME-USP)
- Hércules de
Araujo Feitosa (MAT-UNESP-Bauru)
- Hugo Mariano
(MAT-IME-USP)
- Itala D'Ottaviano (IFCH
and CLE - UNICAMP)
- Odilon Otávio
Luciano (MAT-IME-USP)
- Renata
Wassermann(DCC-IME-USP)
- Post-Doc
Students
- Milton Augustinis de
Castro (IFCH - UNICAMP)
- João Marcos
(IFCH-UNICAMP and IST, Lisbon)
- Luís
Sbardellini (IFCH-UNICAMP)
- PhD
Students
- Adolfo Gustavo Serra
Seca Neto (DCC-IME-USP)
- Carlos Hifume
(IFCH-UNICAMP)
- Eudenia Xavier Meneses
(DCC-IME-USP)
- Joselyto Riani
(DCC-IME-USP)
- Juan Carlos Agudelo
Agudelo (IFCH-UNICAMP)
- Juliana Bueno
(IFCH-UNICAMP)
- Rodrigo de Alvarenga
Freire (IFCH-UNICAMP)
- MSc
Students
- Guilherme Rabello
(MAT-IME-USP)
- Paulo Petrillo
(IFCH-UNICAMP)
- External
Participants
- Amilcar Sernadas (IST,
Lisbon)
- Alexandre Costa-Leite
(Université de Neuchâtel, Switzerland)
- Carlos Caleiro (IST,
Lisbon)
- Cristina Sernadas (IST,
Lisbon)
- Dov Gabbay (King's
College, London)
- Jean-Yves
Béziau (Université de Neuchâtel,
Switzerland)
- João Rasga
(IST, Lisbon)
- Paulo Mateus (IST,
Lisbon)
Considering the background of the people involved and the
intended
objectives stated above, the project will be naturally divided into
three main
tasks, each under the coordination of a senior researcher. Each task
is further subdivided into specific subtasks as detailed below. The
specific participants of each subtask can be found in
Section "Project Description".
- Task 1:
Fundamentals of
Combining
Logics, coordinated by
Marcelo Coniglio. Subtasks:
- Combinations of Logics
and their Applications
- Splitting and
Algebraizing Logics
- Algebraic Semantics for
Modal Logics
- Algebraic and Categorial
Aspects of Logical Consequence
- Task 2:
Computational
Aspects of
Combinations of Logics and Theorem Proving,
coordinated by Marcelo Finger. Subtasks:
- Polynomial-Time
Approximations of Classical Propositional Logic
- First-Order Approximate
Inference
- Resource Sensitive
Inference
- Automatising
Paraconsistent Inference
- Task 3:
Quantum Logics and
Algorithms,
coordinated by Walter Carnielli. Subtasks:
- Quantum Computation and
Quantum Logics
- Polynomial Ring Proof
Procedures
- Paraconsistent Turing
Machines
Project Description
The organization of the research effort into three tasks
with further
subdivision reveals the inherent interconnections and
interdependencies.
Task
1: Fundamentals of Combining Logics
Task
coordinator: Marcelo Coniglio
Subtask:
Combinations of Logics and their Applications
Participants: Marcelo Coniglio, Walter
Carnielli, Dov Gabbay, Cristina
Sernadas, João Rasga, Jean-Yves Béziau, Alexandre
Costa-Leite, Marcelo
Finger, Angela Weiss
Subtask:
Splitting and Algebraizing Logics
Participants: Walter Carnielli,
Marcelo Coniglio, Carlos Caleiro, João Marcos, Juliana Bueno
Subtask: Algebraic
Semantics for Modal Logics
Participants:
Itala D'Ottaviano, Hércules de Araujo Feitosa, Carlos Hifume
Subtask: Algebraic and
Categorial Aspects of Logical Consequence
Participants:
Odilon Otávio Luciano, Hugo Mariano, Marcelo Coniglio,
Luís Sbardellini
Task 2: Computational Aspects of
Combinations of Logics and Theorem Proving
Task coordinator: Marcelo Finger
Subtask: Polynomial-Time
Approximations of Classical Propositional Logic
Participants:
Marcelo Finger, Renata Wassermann, Adolfo Gustavo Serra Seca Neto,
Guilherme Rabello
Subtask: First-Order
Approximate Inference
Participants:
Renata Wassermann, Joselyto Riani, Eudenia Xavier Meneses, Marcelo
Finger
Subtask: Resource
Sensitive Inference
Participants:
Flavio Correa da Silva, Marcelo Finger
Subtask:
Automatizing
Paraconsistent Inference
Participants: Itala Maria Loffredo
D'Ottaviano, Milton Augustinis de Castro
Task 3: Quantum Logics and Algorithms
Task coordinator: Walter Carnielli
Subtask:
Quantum
Computation and Quantum Logics
Participants: Walter Carnielli,
Rodrigo de Alvarenga Freire, Paulo Mateus and Amilcar Sernadas
Subtask:
Polynomial Ring
Proof Procedures
Participants: Walter Carnielli,
Marcelo Coniglio, Paulo Mateus and Cristina
Sernadas
Subtask:
Paraconsistent Turing Machines
Participants:
Walter Carnielli, Juan Carlos Agudelo Agudelo, Paulo Petrillo
-
- BCC04
- J. Bueno, M. E. Coniglio,
and W. A. Carnielli. Finite algebraizability via possible-translations
semantics. In W. A. Carnielli, F. M. Dionísio and P. Mateus,
editors, Proceedings
of CombLog'04 - Workshop on Combination of Logics: Theory and
Applications, pp. 79-86,
Lisbon, Portugal, 2004.
- BJ74
- G. Boolos and R. C.
Jeffrey. Computability
and Logic. Cambridge
University Press, 1974.
(Third edition 1989).
- BP89
- W. J. Blok and D. Pigozzi.
Algebraizable logics. Memoirs
of the American Mathematical Society,
n. 396. 1989.
- Cal00
- C. Caleiro. Combining
Logics.
PhD thesis, IST, Portugal, 2000.
- Car00
- W. A. Carnielli.
Possible-Translations Semantics for Paraconsistent Logics. In D.
Batens, C. Mortensen, G. Priest, and J. P. Van Bendegem, editors, Frontiers of Paraconsistent Logic:
Proceedings of the I World Congress on Paraconsistency,
Logic and Computation Series, pp. 149-163. Baldock: Research Studies
Press, Kings College Publications, 2000.
- Car01
- W. A. Carnielli. Algebraic
proof systems for many-valued logics. I Principia
International Symposium,
Florianópolis, SC, Brazil. Proceedings edited by the
Universidade Federal de Santa Catarina, 2001. pp. 20-24.
- Car90
- W. A. Carnielli.
Many-valued logics and plausible reasoning. In Proceedings
of the XX International
Congress on Many-Valued Logics,
pages 328-335, University of Charlotte, North Carolina, 1990. IEEE
Computer Society Press.
- Car97
- W. A. Carnielli.
Possible-translations semantics for paraconsistent logics. In Frontiers of Paraconsistent Logic
(Ghent, 1997) , volume 8 of Studies in Logic and Computation , pp.
149-163. Research Studies Press, 2000.
- CC99
- W. A. Carnielli and M. E.
Coniglio. A categorial approach to the combination of logics. Manuscrito,
22(2):69-94, 1999.
- CCCSS03
- C. Caleiro, W. A.
Carnielli, M. E. Coniglio, A. Sernadas, and C. Sernadas. Fibring
Non-Truth-Functional Logics: Completeness Preservation. Journal of Logic, Language and
Information, 12(2):183-211,
2003.
- CL99
- W. A. Carnielli and M.
Lima-Marques. Society semantics for multiple-valued logics. In W.A.
Carnielli and I.M.L. DÓttaviano, editors, Advances
in Contemporary Logic and
Computer Science, volume 235
of Contemporary Mathematics Series, pp. 33-52. American Mathematical
Society, 1999.
- CS96
- M. Cadoli and M. Schaerf.
The complexity of entailment in propositional multivalued logics.
Annals of Mathematics and
Artificial Intelligence,
18(1):29-50, 1996.
- CSS03
- M. E. Coniglio, A. Sernadas
and C. Sernadas. Fibring logics with topos semantics. Journal of Logic and Computation,
13(4):595-624, 2003.
- D'A92
- M. D'Agostino.
Are tableaux an improvement on truth-tables? -- cut-free proofs and
bivalence.
Journal of Logic, Language
and Information, 1:235-252,
1992.
- Dal96a
- M. Dalal.
Anytime families of tractable propositional reasoners.
In International Symposium of
Artificial Intelligence and Mathematics AI/MATH-96,
pp. 42-45, 1996.
- Dal96b
- M. Dalal.
Semantics of an anytime family of reasoners.
In 12th European Conference
on Artificial Intelligence,
pp. 360-364, 1996.
- dCFK92
- N. C. A. da Costa, S.
French, and D. Krause. The Schroedinger problem. In M. Bibtol and O.
Darrigol (eds), Erwin Schroedinger: Philosophy
and the Birth of Quantum
Mechanics, Editions
Frontieres, pp. 445-460, 1992.
- DGG04
- M. L. Dalla Chiara, R.
Giuntini and R. Greechie. Reasoning in Quantum
Theory.
Kluwer Academic Publishers, 2004.
- DM94
- M. D'Agostino and M.
Mondadori.
The taming of the cut. Classical refutations with analytic cut.
Journal of Logic and
Computation, 4:285-319, 1994.
- FC03
- V. L. Fernández
and M. E. Coniglio. Combining valuations with society semantics. Journal of Applied Non-Classical Logics,
13(1):21-46, 2003.
- FC04
- V. L. Fernández
and M. E. Coniglio. Fibring algebraizable consequence systems. In W. A.
Carnielli, F. M. Dionísio, and P. Mateus, editors, Proceedings of CombLog'04 - Workshop
on Combination of Logics: Theory and Applications,
pp. 93-98, Lisbon, Portugal, 2004.
- FD01
- H. A. Feitosa and I. M. L.
D'Ottaviano. Conservative translations. Annals
of Pure and Applied Logic
108(1-3):205-227, 2001.
- FW01
- M. Finger and R. Wassermann.
Tableaux for approximate reasoning.
In L. Bertossi and J. Chomicki, editors, IJCAI-2001
Workshop on Inconsistency in Data and Knowledge,
pp. 71-79, Seattle, August 6-10 2001.
- FW02
- M. Finger and R. Wassermann.
Expressivity and control in limited reasoning.
In F. van Harmelen, editor, 15th
European Conference on Artificial Intelligence (ECAI02),
pp. 272-276, Lyon, France, 2002. IOS Press.
- FW04
- M. Finger and R. Wassermann.
Approximate and limited reasoning: Semantics, proof theory,
expressivity and control.
Journal of Logic And
Computation, 14(2):179-204,
2004.
- Gab96
- D. Gabbay. Fibred semantics
and the weaving of logics: Part 1. Journal of
Symbolic Logic,
61(4):1057-1120, 1996.
- Gol74
- R. Goldblatt. Semantics
analysis of orthologic. Journal
of Philosophical Logic 3,
19-35, 1974.
- Gol84
- R. Goldblatt.
Orthomodularity is not elementary. Journal of
Symbolic Logic
49, 401-404, 1984.
- Gra87
- J. W. Gray. Categorical
aspects of data type
constructors. Theoretical
Computer Science 50:103-135,
1987.
- Gra89
- J. W. Gray. The Category of
Sketches as model for algebraic
semantics. Contemporary
Mathematics 92:109-135, 1989.
- Gro97
- L. K. Grover. Quantum
Mechanics Helps in Searching for a Needle in a Haystack. Physical Review Letters
Volume 79, Number 2, 14 July 1997.
- GKWZ
- D. Gabelaia,
A. Kurucz, F. Wolter, and M. Zakharyaschev.
Products of transitive modal logics.
in submission.
- HP89
- J. Martin, E. Hyland, A. M.
Pitts. The Theory of Constructions:
Categorical Semantics and Topos-theoretic models. Contemporary
Mathematics 92:137-199, 1989.
- KW91
- M. Kracht and
F. Wolter.
Properties of independently axiomatizable bimodal logics.
Journal of Symbolic Logic,
56(4):1469-1485, 1991.
- Mas98
- F. Massacci.
Efficient Approximate
Deduction and an Application to Computer Security.
PhD thesis, Dottorato in Ingegneria Informatica, Università
di Roma I ``La Sapienza'', Dipartimento di Informatica e Sistemistica,
June 1998.
- MS
- P. Mateus and A. Sernadas. Exogenous
Quantum Logic.
Manuscript. CLC, Department of Mathematics, IST. Available at http://wslc.math.ist.utl.pt/ftp/pub/SernadasA/04-MS-fiblog24s.pdf.
- SCV99
- A. M. Sette, W. A.
Carnielli and P. Veloso. An alternative view of default reasoning and
its logic. In: E. H. Hauesler and L. C. Pereira, (Eds.) Pratica:
Proofs, types and categories.
Rio de Janeiro: PUC. pp. 127-158, 1999.
- Sho94
- P. W. Shor. Algorithms for
quantum computation: Discrete logarithms and factoring, Proc. 35nd Annual Symposium on
Foundations of Computer Science
(Shafi Goldwasser, ed.), IEEE Computer Society Press (1994), 124-134.
- Sho97
- P. W. Shor. Polynomial-time
algorithms for prime factorization and discrete logarithms on a quantum
computer. SIAM
Journal on Computing,
26(5):1484-1509, 1997.
- Smu68
- R. M. Smullyan.
First-Order Logic.
Springer-Verlag, 1968.
- SSC99
- A. Sernadas, C. Sernadas
and C. Caleiro. Fibring of logics as a categorial construction. Journal of Logic and Computation,
9(2):149-179, 1999.
- SSZ02
- A. Sernadas, C. Sernadas
and A. Zanardo. Fibring modal first-order logics: Completeness
preservation. Logic
Journal of the IGPL,
10(4):413-451, 2002.
- VC04
- P. A. S. Veloso and W. A.
Carnielli. Logics for Qualitative Reasoning. In S. Rahman et al.,
editors, Logic,
Epistemology and the Unity of Science.
Kluwer Academic Publishers, pp. 487-526, 2004.
- Was00
- R. Wassermann. Resource-Bounded
Belief
Revision,
PhD
Thesis, University of Amsterdam, 2000.
- Wol96
- Frank Wolter.
Fusions of modal logics revisited.
In Advances in Modal Logic,
volume Volume 1 of Lecture
Notes 87, pages 361-379. CSLI
Publications, Stanford, CA, 1996.
- ZSS99
- A. Zanardo, A. Sernadas,
and C. Sernadas. Fibring: Completeness preservation. Journal of Symbolic Logic,
66(1):414-439, 2001.