Current Research Projects

ConsRel - Logical Consequence and Combinations of Logics

FAPESP Project Number: 2004/14107-2. Institution: Centro de Lógica, Epistemologia e História da Ciência - Unicamp. Area: 07010000 - Philosophy. Period: 01/04/2005 - 31/03/2009

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.

The technique provides an effective compromise between fidelity and time requirements, producing high quality approximations with great flexibility.

More info about this project: ConsRel home page.

KEMS - A KE-based Multi-Strategy Theorem Prover

KEMS is a KE-based Multi-Strategy theorem prover. The KE system, a tableau method developed by Marco Mondadori and Marcello D'Agostino [1], was presented as an improvement, in the computational efficiency sense, over the Analytic Tableau method [2]. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. A multi-strategy theorem prover can be used for three purposes: educational, exploratory and adaptive. For educational purposes, it can be used to illustrate how the choice of a strategy can affect performance of the prover. As an exploratory tool, a multi-strategy theorem prover can be used to test new strategies and compare them with others. And we can also think of an adaptive multi-strategy theorem prover that changes the strategy used according to features of the problem presented to it.

KEMS is part of Adolfo Gustavo Serra Seca Neto's PhD. project, advised by Marcelo Finger. The KEMS is implemented in Java and AspectJ. Java is a well established object-oriented programming language and AspectJ is the major representative of a new programming paradigm: aspect-oriented programming.

[1] The Taming of the Cut. Classical Refutations with Analytic Cut Journal of Logic and Computation, vol. 4, number 3, pp. 285-319, 1994

[2] First-Order Logic, Raymond Smullyan. Dover Publications, 1968

More info about this project: KEMS home page.

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License