Comparing instance generation methods for automated reasoning

DOI10.1007/S10817-006-9046-XzbMATH Open1113.68089OpenAlexW2006807333MaRDI QIDQ877884FDOQ877884

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

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

zbMATH Keywords

disconnection tableau calculustableau-based methods

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• A machine program for theorem-proving
• Ordered semantic hyper-linking
• Title not available (Why is that?)
• Proof and model generation with disconnection tableaux
• Title not available (Why is that?)
• Eliminating dublication with the hyper-linking strategy
• The model evolution calculus.
• Partial instantiation methods for inference in first-order logic
• Automated Reasoning
• Automated Reasoning with Analytic Tableaux and Related Methods

Cited In (8)

• What is essential unification?
• Set of support, demodulation, paramodulation: a historical perspective
• Title not available (Why is that?)
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Semantically-guided goal-sensitive reasoning: model representation
• Automated Reasoning with Analytic Tableaux and Related Methods
• A combined superposition and model evolution calculus
• Craig interpolation with clausal first-order tableaux

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)