Consolution as a framework for comparing calculi

DOI10.1006/JSCO.1993.1058MaRDI QIDQ1322772zbMATH OpenOpenAlexFDO

Authors Peter Baumgartner, Ulrich Furbach

Publication date 5 May 1994

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1006/jsco.1993.1058

zbMATH Keywords

connection methodconsolution calculusfirst-order proof calculimodel eliminationresolutiontableaux model elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited in

(10)

• Computing answers with model elimination
• Linear and unit-resulting refutations for Horn theories
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Semantically-guided goal-sensitive reasoning: model representation
• scientific article; zbMATH DE number 4209640 (Why is no real title available?)
• scientific article; zbMATH DE number 48763 (Why is no real title available?)
• scientific article; zbMATH DE number 67453 (Why is no real title available?)
• Model elimination without contrapositives
• What you always wanted to know about rigid \(E\)-unification
• Display calculi and other modal calculi: a comparison

Describes a project that uses

Uses Software

• SETHEO

This page was built for publication: Consolution as a framework for comparing calculi

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