Table of Contents

Description
KEMS is a KEbased MultiStrategy 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 multistrategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. A multistrategy 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 multistrategy theorem prover can be used to test new strategies and compare them with others. And we can also think of an adaptive multistrategy theorem prover that changes the strategy used according to features of the problem presented to it.
KEMS was part of Adolfo Gustavo Serra Seca Neto's PhD. project, advised by Marcelo Finger. KEMS is implemented in Java and AspectJ. Java is a well established objectoriented programming language and AspectJ is the major representative of a new programming paradigm: aspectoriented programming. Currently, it is being developed under the auspices of the ConsRel project.
[2] FirstOrder Logic, Raymond Smullyan. Dover Publications, 1968.
For more information about KEMS click here. Note: March 25, 2009. This site is having some problems…
News
 March 22th, 2010: KEMS as a Java Web Start application
 Note: If you don't see the Java Web Start application running, make sure that you have at least the Java 2 Platform, Standard Edition (J2SE) 1.4.2 release on your machine. If not, download and install the latest release of the Java SE Development Kit (JDK).
 The conversion of the KEMS jar file into a Java Web Start application was done mainly by Emerson Shigueo Sugimoto.
KEMS source code and executables
 KEMS at GitHub
 Use git or click here to donwload KEMS's latest version with source code (as a zip file)
 To run KEMS do the following:

 Unzip the zip file
 Go to the KEMS/kems.export/ folder
 Issue the following command: java jar kems.jar

 To run KEMS do the following:
 Use git or click here to donwload KEMS's latest version with source code (as a zip file)
 If you want to participate in the KEMS project, please contact the project leader at adolfo.usp @ gmail.com
 New! How to install and use KEMS  Video (in Portuguese): http://ifile.it/scf5b8a
Related Publications
PhD. Dissertation
 Adolfo Gustavo Serra Seca Neto's Ph.D. Thesis: A MultiStrategy Tableau Prover
 Official version at USP: http://www.teses.usp.br/teses/disponiveis/45/45134/tde04052007175943/
 Advisor: Marcelo Finger
 Institute of Mathematics and Statistics (IME) Univerisity of São Paulo (USP)
 January 30th, 2007
Papers and reports
 NETO, Adolfo. KEMS  Um demonstrador de teoremas multiestratégia FREEBASE 2010. Disponível em: < http://bit.ly/aoaJMO >. Acesso em: 12 ago. 2010.
 NETO, ADOLFO ; Kaestner, Celso A.A. ; FINGER, Marcelo . Towards an Efficient Prover for the C1 Paraconsistent Logic. Electronic Notes in Theoretical Computer Science, v. 256, p. 87102, 2009.
 NETO, ADOLFO ; KAESTNER, C. A. A. ; FINGER, Marcelo . Towards an efficient prover for the C1 paraconsistent logic. In: Workshop on Logical and Semantic Frameworks, with Applications (LSFA), 2009, Brasília. Procedings of LSFA'09, 2009.
 NETO, ADOLFO ; FINGER, Marcelo . Effective Prover for Minimal Inconsistency Logic. In: Max Bramer. (Org.). Artificial Intelligence in Theory and Practice. : Springer, 2006, v. 217, p. 465474.
 NETO, ADOLFO ; FINGER, Marcelo . KEMS  A MultiStrategy Tableau Prover. In: VI Best MSc Dissertation/PhD Thesis Contest (CTDIA 2008), 2008, Salvador, Bahia. WTDIA & CTDIA Proceedings, 2008.
 NETO, ADOLFO G. S. S. ; FINGER, Marcelo . A KE Tableau for a Logic of Formal Inconsistency. In: TABLEAUX 2007  Automated Reasoning with Analytic Tableaux and Related Methods, 2007, Aix en Provence. Proceedings of TABLEAUX'07 position papers and Workshop on Agents, Logic and Theorem Proving. Marseille : Technical Report (LSIS.RR.2007.002) of the LSIS/Université Paul Cézanne, 2007.
 NETO, ADOLFO ; FINGER, Marcelo . Effective Prover for Minimal Inconsistency Logic. In: IFIP AI 2006 (part of IIFIP 19th World Computer Congress, 2006), 2006, Santiago, Chile. ARTIFICIAL INTELLIGENCE IN THEORY AND PRACTICE. Boston : Springer, 2006. p. 465474.
 NETO, ADOLFO G. S. S. ; FINGER, Marcelo . Implementing a MultiStrategy Theorem Prover. In: Encontro Nacional de Inteligência Artificial  ENIA, 2005, São Leopoldo  RS. Anais do V Encontro Nacional de Inteligência Artificial, 2005. p. 861871.
 NETO, ADOLFO G. S. S. ; FINGER, Marcelo . Using AspectOriented Programming in the Development of a MultiStrategy Theorem Prover. In: II Jornada do Conhecimento e da Tecnologia, 2005, MaríliaSP. Anais da II Jornada do Conhecimento e da Tecnologia, 2005.
 NETO, ADOLFO G. S. S. ; FINGER, Marcelo . Effective Prover for Logics of Formal Inconsistency. In: II SIMPÓSIO DE INICIAÇÃO CIENTÍFICA E PÓSGRADUAÇÃO DO IMEUSP, 2006, São Paulo. II SIMPÓSIO DE INICIAÇÃO CIENTÍFICA E PÓSGRADUAÇÃO DO IMEUSP, 2006.
 NETO, ADOLFO G. S. S. . A MultiStrategy Tableau Prover. In: I Simpósio de Iniciação Científica e PósGraduação do IMEUSP, 2005, São Paulo. I Simpósio de Iniciação Científica e PósGraduação do IMEUSP, 2005.
 NETO, ADOLFO G. S. S. . A MultiStrategy Theorem Prover. In: Workshop Semantics and Meaning, 2005, Campinas. Workshop Semantics and Meaning, 2005.
Several of the publications above can be downloaded at http://www.dainf.ct.utfpr.edu.br/~adolfo/publications/
Problems (and families of problems) for evaluating theorem provers for classical and paraconsistent propositional logics
A large set of problems than can be used to evaluate theorem provers for classical and paraconsistent propositional logics is available in http://github.com/adolfont/KEMS/tree/master/kems.problems/problems/.
Problem format accepted by KEMS
The user can enter a problem either using SATLIB CNF format or in an extension of the format used in Wagner Dias's MSc. Dissertation.
To enter a problem (either in the Problem Editor window or when editing a problem file in any text editor) using the extension of the format of Wagner Dias,
one must provide a list of signed formulas (sformulas). Each line can contain at most one sformula.
Comment lines start with a #. A signed formula is a sign followed by a formula. The allowed signs are T (true) and F (false).
Formulas can be atomic or composite. An atomic formula is a string of letters and numbers initiated by a letter. Composite formulas have a connective and zero, one or two
subformulas (which are themselves formulas). The notation for composite formulas is the common infix notation. For zeroary connectives, a formula is its Connective. For unary
connectives, Connective Formula. And for binary connectives, Formula Connective Formula. Parentheses are used when necessary to establish precedence.
The allowed connectives are:
 zeroary: TOP and BOTTOM;
 unary: ! (not), @ (consistency) and * (inconsistency);
 binary: & (and),  (or), > (implication), <=> (biimplication) and + (exclusive or).
The following is an example of a CPL problem:
T A <=> (B&!C)
T TOP> !(AD)
F BOTTOM  (!D)
And here we can see an example of a mbC (or mCi) problem:
T A <=> @(B&!*C)
T TOP> !(A@D)
F BOTTOM  @(!D)
In mbC and mCi, ‘*A’ is translated into ‘!@A’. The previous problem can also be submitted to a CPL strategy: ‘@A’ formulas will be translated into ‘TOP’ and ‘*A’ into
‘BOTTOM’.
For the C1 logic (a propositional paraconsistent logic), only the following connectives are allowed:
 zeroary: TOP and BOTTOM;
 unary: ! (not), @ (consistency) and * (inconsistency);
 binary: & (and),  (or), > (implication), <=> (biimplication) and + (exclusive or).
Therefore, the following connectives are only allowed for CPL, mbC and mCi problems:
 zeroary: TOP and BOTTOM;
 unary: @ (consistency) and * (inconsistency);
 binary: <=> (biimplication) and + (exclusive or).
An example of a problem for C1 (which can be found in http://github.com/adolfont/KEMS/blob/master/kems.problems/problems/generated/lfiProblems/family5/family5_03.prove) is:
T !(A1&!A1)
T A1&A2&A3
T (A4> ((A1B1)>(!(A2&!A2))))&(A4> ((A2B2)>(!(A3&!A3))))&(A4> ((A3B3)>(!(A4&!A4))))
T (!(A1&!A1)&!(A2&!A2)&!(A3&!A3))>(!A4)
F !!!A4
This problem is a representation of the following sequent: