Efficient model generation through compilation.

DOI10.1006/INCO.1999.2863zbMath1045.68605OpenAlexW2066884140MaRDI QIDQ1854374

Tim Geisler, Heribert Schütz

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1999.2863

zbMATH Keywords

TPTP problem librarySatchmotableau-based model generators

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mechanization of proofs and logical operations (03B35)

Related Items (1)

An efficient relational deductive system for propositional non-classical logics

Uses Software

• SETHEO
• TPTP
• SATCHMO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• SATCHMORE: SATCHMO with RElevancy
• Using resolution for deciding solvable classes and building finite models
• Minimal model generation with positive unit hyper-resolution tableaux
• The design of the CADE-13 ATP system competition
• Hyperresolution and automated model building
• The TPTP problem library
• LeanT A P: Lean tableau-based theorem proving
• Hyper tableaux

This page was built for publication: Efficient model generation through compilation.