SETHEO: A high-performance theorem prover

DOI10.1007/BF00244282zbMath0759.68080MaRDI QIDQ1189726

S. Singh

Publication date: 27 September 1992

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

Prolog; preprocessing; first order logic; connection method; abstract machine technology; model elimination

Mathematics Subject Classification ID

Related Items

An automatic proof of Gödel's incompleteness theorem, Controlled use of clausal lemmas in connection tableau calculi, A Prolog technology theorem prover: A new exposition and implementation in Prolog, Let's plan it deductively!, Prolog technology for default reasoning: proof theory and compilation techniques, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Controlled integration of the cut rule into connection tableau calculi, Clause trees: A tool for understanding and implementing resolution in automated reasoning, Non-Horn clause logic programming, Computing answers with model elimination, IeanCOP: lean connection-based theorem proving, Evaluating general purpose automated theorem proving systems, Towards the qualitative, plan-based simulation of international crises, A uniform procedure for converting matrix proofs into sequent-style systems, A new methodology for query answering in default logics via structure-oriented theorem proving, lean\(T^ AP\): Lean tableau-based deduction, Linear and unit-resulting refutations for Horn theories, Near-Horn Prolog and the ancestry family of procedures, Knowledge-based proof planning

Uses Software

• SETHEO