Comparing instance generation methods for automated reasoning

DOI10.1007/S10817-006-9046-XMaRDI QIDQ877884zbMATH OpenOpenAlexFDO

Authors Swen Jacobs, Uwe Waldmann

Publication date 4 May 2007

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

Full work available at URL http://edoc.mpg.de/279121

zbMATH Keywords

disconnection tableau calculustableau-based methods

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Automated Reasoning with Analytic Tableaux and Related Methods
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• scientific article; zbMATH DE number 2165692
• Combining instance generation and resolution
• Computer Science Logic

Cites work

• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• scientific article; zbMATH DE number 1950261 (Why is no real title available?)
• A machine program for theorem-proving
• Automated Reasoning
• Automated Reasoning with Analytic Tableaux and Related Methods
• Eliminating dublication with the hyper-linking strategy
• Ordered semantic hyper-linking
• Partial instantiation methods for inference in first-order logic
• Proof and model generation with disconnection tableaux
• The model evolution calculus.

Cited in

(8)

• Craig interpolation with clausal first-order tableaux
• A combined superposition and model evolution calculus
• Semantically-guided goal-sensitive reasoning: model representation
• What is essential unification?
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Set of support, demodulation, paramodulation: a historical perspective
• Automated Reasoning with Analytic Tableaux and Related Methods
• scientific article; zbMATH DE number 1256721 (Why is no real title available?)

This page was built for publication: Comparing instance generation methods for automated reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877884)