A new clausal class decidable by hyperresolution

DOI10.1007/3-540-45620-1_21MaRDI QIDQ4809060zbMATH OpenFDO

Authors Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2392/23920260.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Resolution decision procedures
• scientific article; zbMATH DE number 440110
• scientific article; zbMATH DE number 515732
• Hyperresolution and automated model building
• BDI: a new decidable clause class

Cited in

(9)

• A new methodology for developing deduction methods
• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• BDI: a new decidable clause class
• Simulation and synthesis of deduction calculi
• First-order resolution methods for modal logics
• A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
• First-order automatic literal model generation
• Representing and building models for decidable subclasses of equational clausal logic
• Some techniques for proving termination of the hyperresolution calculus

This page was built for publication: A new clausal class decidable by hyperresolution

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