Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
From MaRDI portal
Publication:5507985
DOI10.1145/321296.321302zbMath0135.18401OpenAlexW1972956465WikidataQ114255236 ScholiaQ114255236MaRDI QIDQ5507985
No author found.
Publication date: 1965
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321296.321302
Related Items (54)
Semantically-guided goal-sensitive reasoning: model representation ⋮ The resonance strategy ⋮ Goal directed strategies for paramodulation ⋮ Hierarchical deduction ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ Resolution vs. cutting plane solution of inference problems: Some computational experience ⋮ Case splitting in an automatic theorem prover for real-valued special functions ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ On First-Order Model-Based Reasoning ⋮ On structures of regular standard contradictions in propositional logic ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Theorem proving with abstraction ⋮ Unnamed Item ⋮ Automation for interactive proof: first prototype ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ An epistemic model of logic programming ⋮ Checking the quality of clinical guidelines using automated reasoning tools ⋮ A resolution framework for finitely-valued first-order logics ⋮ A semantic backward chaining proof system ⋮ The Strategy Challenge in SMT Solving ⋮ Canonical Ground Horn Theories ⋮ A relaxation approach to splitting in an automatic theorem prover ⋮ Sledgehammer: Judgement Day ⋮ Experimental tests of resolution-based theorem-proving strategies ⋮ A complete semantic back chaining proof system ⋮ Parallelizing the closure computation in automated deduction ⋮ SLIM: An automated reasoner for equivalences, applied to set theory ⋮ Hyper resolution and equality axioms without function substitutions ⋮ A logical framework for depiction and image interpretation ⋮ Removing irrelevant information in temporal resolution proofs ⋮ A pragmatic approach to resolution-based theorem proving ⋮ Lightweight relevance filtering for machine-generated resolution problems ⋮ The search efficiency of theorem proving strategies ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ : A Resolution-Based Prover for Multimodal K ⋮ Generalized completeness for SOS resolution and its application to a new notion of relevance ⋮ Resolution graphs ⋮ Finding resolution proofs and using duplicate goals in AND/OR trees ⋮ Experiments with a heuristic theorem-proving program for predicate calculus with equality ⋮ Linear resolution with selection function ⋮ Theorem proving with variable-constrained resolution ⋮ Beweisalgorithmen für die Prädikatenlogik ⋮ Layered clause selection for theory reasoning (short paper) ⋮ The application of automated reasoning to formal models of combinatorial optimization ⋮ A typed resolution principle for deduction with conditional typing theory ⋮ A mechanical solution of Schubert's steamroller by many-sorted resolution ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ The kernel strategy and its use for the study of combinatory logic ⋮ Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL ⋮ Semantic relevance ⋮ MRPPS?An interactive refutation proof procedure system for question-answering
This page was built for publication: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
