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.
[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…
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)
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:
