Resolution Strategies as Decision Procedures

DOI10.1145/321958.321960zbMath0335.68062OpenAlexW2123319860MaRDI QIDQ4102765

William H. Jun. Joyner

Publication date: 1976

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/321958.321960

Mathematics Subject Classification ID

Related Items (33)

History and Prospects for First-Order Automated Deduction ⋮ Proof normalization for resolution and paramodulation ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Using resolution for deciding solvable classes and building finite models ⋮ Some techniques for proving termination of the hyperresolution calculus ⋮ Structured proof procedures ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Logical reduction of metarules ⋮ An algorithm for the retrieval of unifiers from discrimination trees ⋮ Automatic theorem proving. II ⋮ Deciding expressive description logics in the framework of resolution ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Semantic trees revisited: Some new completeness results ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ Removing redundancy from a clause ⋮ The Blossom of Finite Semantic Trees ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically ⋮ Tractable query answering and rewriting under description logic constraints ⋮ Maslov's inverse method and decidable classes ⋮ Semantic tableaux with ordering restrictions ⋮ SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation ⋮ Unsorted Functional Translations ⋮ Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic ⋮ A classification of non-liftable orders for resolution ⋮ Loop checking in SLD-derivations by well-quasi-ordering of goals ⋮ Deciding the \(E^+\)-class by an a posteriori, liftable order ⋮ Rewriting Conjunctive Queries over Description Logic Knowledge Bases ⋮ A theory of data dependencies over relational expressions ⋮ SGGS decision procedures ⋮ The complexity of the satisfiability problem for Krom formulas ⋮ Set of support, demodulation, paramodulation: a historical perspective

This page was built for publication: Resolution Strategies as Decision Procedures