Sciweavers

CADE
1998
Springer
14 years 3 months ago
Strict Basic Superposition
It is a well-known fact that some form of factoring is necessary for completeness of paramodulation-based calculi of general first-order clauses. In this paper we give an overview...
Leo Bachmair, Harald Ganzinger
CADE
1998
Springer
14 years 3 months ago
System Description: LEO - A Higher-Order Theorem Prover
Christoph Benzmüller, Michael Kohlhase
CADE
1998
Springer
14 years 3 months ago
System Description: leanK 2.0
Abstract. leanK is a "lean", i.e., extremely compact, Prolog implementation of a free variable tableau calculus for propositional modal logics. leanK 2.0 includes additio...
Bernhard Beckert, Rajeev Goré