Eliminating dublication with the hyper-linking strategy
From MaRDI portal
Publication:688547
DOI10.1007/BF00247825zbMath0784.68077MaRDI QIDQ688547
Shie-Jue Lee, David Alan Plaisted
Publication date: 2 January 1994
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
theorem provinglinksDavis-Putnam procedureduplication by case analysisduplication by combinationhyper- linkinginstancespropositional calculus decision procedure
Related Items (28)
Semantically-guided goal-sensitive reasoning: model representation ⋮ Problem solving by searching for models with a theorem prover ⋮ Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures ⋮ History and Prospects for First-Order Automated Deduction ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ The model evolution calculus as a first-order DPLL method ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ Unnamed Item ⋮ Comparing instance generation methods for automated reasoning ⋮ The disconnection tableau calculus ⋮ Many-valued logic and mixed integer programming ⋮ Structured proof procedures ⋮ On First-Order Model-Based Reasoning ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ What Is Essential Unification? ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ The Relative Power of Semantics and Unification ⋮ Toward leaner binary-clause reasoning in a satisfiability solver ⋮ The search efficiency of theorem proving strategies ⋮ Semantically guided first-order theorem proving using hyper-linking ⋮ A typed resolution principle for deduction with conditional typing theory ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ SMELS: satisfiability modulo equality with lazy superposition ⋮ SET-VAR
This page was built for publication: Eliminating dublication with the hyper-linking strategy
