Some techniques for proving termination of the hyperresolution calculus

DOI10.1007/s10817-006-9028-zzbMath1112.03012OpenAlexW2051480593MaRDI QIDQ861692

Nicolas Peltier

Publication date: 30 January 2007

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

Full work available at URL: https://doi.org/10.1007/s10817-006-9028-z

zbMATH Keywords

complexity measuresdecision procedureshyperresolution

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Uses Software

• SATCHMO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resolution methods for the decision problem
• Hyperresolution for guarded formulae
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Using resolution for testing modal satisfiability and building models
• SHR Tableaux -- A Framework for Automated Model Generation
• An Efficient Unification Algorithm
• Resolution Strategies as Decision Procedures
• A strong version of Herbrand's theorem for introvert sentences
• Termination of logic programs: the never-ending story
• Hyperresolution and automated model building
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Some techniques for proving termination of the hyperresolution calculus