Proving refutational completeness of theorem-proving strategies
From MaRDI portal
Publication:4302847
DOI10.1145/116825.116833zbMath0799.68170OpenAlexW2043314428MaRDI QIDQ4302847
Jieh Hsiang, Michaël Rusinowitch
Publication date: 21 August 1994
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/116825.116833
completenessresolutionHorn logicparamodulationfirst-order logic with equalitytransfinite ordinalstransfinite semantic treescomplete simplification orderingsfunctional reflexive axiomsrefutational theorem proving strategiesWos-Robinson conjecture
Related Items
Conditional term rewriting and first-order theorem proving ⋮ Clausal rewriting ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Automated deduction with associative-commutative operators ⋮ Proof normalization for resolution and paramodulation ⋮ Goal directed strategies for paramodulation ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Paramodulation with non-monotonic orderings and simplification ⋮ Reasoning with conditional axioms ⋮ On First-Order Model-Based Reasoning ⋮ From diagrammatic confluence to modularity ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Redundancy criteria for constrained completion ⋮ Semantic trees revisited: Some new completeness results ⋮ On the complexity of recursive path orderings ⋮ The Blossom of Finite Semantic Trees ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Abstract canonical presentations ⋮ The search efficiency of theorem proving strategies ⋮ Ordered chaining for total orderings ⋮ Associative-commutative deduction with constraints ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Model completeness, covers and superposition ⋮ Local simplification ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ Theorem-proving with resolution and superposition ⋮ Local simplification ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II ⋮ Deductive and inductive synthesis of equational programs
