Automated deduction by theory resolution

DOI10.1007/BF00244275zbMath0616.68076OpenAlexW2047669821MaRDI QIDQ1821564

Mark E. Stickel

Publication date: 1985

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244275

zbMATH Keywords

decision proceduresresolution theorem-proving

Mathematics Subject Classification ID

Related Items (48)

A resolution principle for constrained logics ⋮ Refutational theorem proving for hierarchic first-order theories ⋮ Hybrid reasoning using universal attachment ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Link inheritance in abstract clause graphs ⋮ Hybridizing nonmonotonic inheritance with theorem proving ⋮ Unification modulo an equality theory for equational logic programming ⋮ A new reduction rule for the connection graph proof procedure ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ On Skolemization in constrained logics ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Defining answer classes using resolution refutation ⋮ Structured proof procedures ⋮ Unification properties of commutative theories: A categorical treatment ⋮ Unification in varieties of completely regular semigroups ⋮ Computing answers with model elimination ⋮ Axiomatic Constraint Systems for Proof Search Modulo Theories ⋮ Deterministic statistical mapping of sentences to underspecified semantics ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Theorem proving modulo ⋮ The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning ⋮ Reduction rules for resolution-based systems ⋮ Cyclic connections ⋮ Incremental theory reasoning methods for semantic tableaux ⋮ An order-sorted logic for knowledge representation systems ⋮ Unification theory ⋮ Proof normalization modulo ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ A Prolog technology theorem prover: A new exposition and implementation in Prolog ⋮ Theory matrices (for modal logics) using alphabetical monotonicity ⋮ Canonical Ground Horn Theories ⋮ The Relative Power of Semantics and Unification ⋮ The ECO family ⋮ Exploiting lattices in a theory of space and time ⋮ Completing sort hierarchies ⋮ Connection calculus theorem proving with multiple built-in theories ⋮ Constraint solving for proof planning ⋮ Building Theorem Provers ⋮ Unification in commutative theories ⋮ Primal grammars and unification modulo a binary clause ⋮ A practical integration of first-order reasoning and decision procedures ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ Swinging types=functions+relations+transition systems ⋮ Efficient algorithms for qualitative reasoning about time ⋮ A typed resolution principle for deduction with conditional typing theory ⋮ A mechanical solution of Schubert's steamroller by many-sorted resolution ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Logic-based subsumption architecture

This page was built for publication: Automated deduction by theory resolution