KEMS

Description

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 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 object-oriented programming language and AspectJ is the major representative of a new programming paradigm: aspect-oriented programming. Currently, it is being developed under the auspices of the ConsRel project.

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

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

  • If you want to participate in the KEMS project, please contact the project leader at adolfo.usp @ gmail.com

Related Publications

PhD. Dissertation

Papers and reports

  • NETO, Adolfo. KEMS - Um demonstrador de teoremas multi-estraté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. 87-102, 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. 465-474.
  • NETO, ADOLFO ; FINGER, Marcelo . KEMS - A Multi-Strategy 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. 465-474.
  • NETO, ADOLFO G. S. S. ; FINGER, Marcelo . Implementing a Multi-Strategy 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. 861-871.
  • NETO, ADOLFO G. S. S. ; FINGER, Marcelo . Using Aspect-Oriented Programming in the Development of a Multi-Strategy Theorem Prover. In: II Jornada do Conhecimento e da Tecnologia, 2005, Marília-SP. 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ÓS-GRADUAÇÃO DO IME-USP, 2006, São Paulo. II SIMPÓSIO DE INICIAÇÃO CIENTÍFICA E PÓS-GRADUAÇÃO DO IME-USP, 2006.
  • NETO, ADOLFO G. S. S. . A Multi-Strategy Tableau Prover. In: I Simpósio de Iniciação Científica e Pós-Graduação do IME-USP, 2005, São Paulo. I Simpósio de Iniciação Científica e Pós-Graduação do IME-USP, 2005.
  • NETO, ADOLFO G. S. S. . A Multi-Strategy 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 (s-formulas). Each line can contain at most one s-formula.

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), <=> (bi-implication) and + (exclusive or).

The following is an example of a CPL problem:
T A <=> (B&!C)
T TOP-> !(A|D)
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), <=> (bi-implication) 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: <=> (bi-implication) 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-> ((A1|B1)->(!(A2&!A2))))&(A4-> ((A2|B2)->(!(A3&!A3))))&(A4-> ((A3|B3)->(!(A4&!A4))))
T (!(A1&!A1)&!(A2&!A2)&!(A3&!A3))->(!A4)
F !!!A4

This problem is a representation of the following sequent:

family5_3.gif

Software used in KEMS development

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