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.

1. 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.

2. 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.

3. 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".

1. 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

2. 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

3. 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

Bibliography

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.