A sequent-style model elimination strategy and a positive refinement
From MaRDI portal
Publication:2639044
DOI10.1007/BF00244355zbMath0718.03011MaRDI QIDQ2639044
Publication date: 1990
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
mechanical theorem provingmodel eliminationgoal-subgoal structureMESON proceduresequent style proof system
Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)
Related Items (11)
TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic ⋮ Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Near-Horn Prolog and the ancestry family of procedures ⋮ Avoiding duplicate proofs with the foothold refinement ⋮ Non-Horn clause logic programming ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ A semantic backward chaining proof system ⋮ Optimizing proof search in model elimination ⋮ A Prolog technology theorem prover: A new exposition and implementation in Prolog ⋮ Model elimination without contrapositives
This page was built for publication: A sequent-style model elimination strategy and a positive refinement
