Consolution as a framework for comparing calculi
From MaRDI portal
Publication:1322772
DOI10.1006/jsco.1993.1058zbMath0803.68120OpenAlexW2153361692MaRDI QIDQ1322772
Ulrich Furbach, Peter Baumgartner
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
resolutionconnection methodmodel eliminationconsolution calculusfirst-order proof calculitableaux model elimination
Related Items
Semantically-guided goal-sensitive reasoning: model representation ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Computing answers with model elimination ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Model elimination without contrapositives ⋮ What you always wanted to know about rigid E-unification
Uses Software
