Automatic Theorem Proving With Renamable and Semantic Resolution

DOI10.1145/321420.321428zbMath0157.02405OpenAlexW2020794409MaRDI QIDQ5538933

James R. Slagle

Publication date: 1967

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

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

zbMATH Keywords

mathematical logic

Related Items (36)

Semantically-guided goal-sensitive reasoning: model representation ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ One modification of the ordering strategy in the resolution method ⋮ On First-Order Model-Based Reasoning ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ On structures of regular standard contradictions in propositional logic ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Theorem proving with abstraction ⋮ Unnamed Item ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ Completeness of resolution revisited ⋮ Solving SAT by algorithm transform of Wu's method ⋮ Multi-ary α-semantic resolution automated reasoning based on lattice-valued first-order logic LF (X)1 ⋮ Separable resolution method for checking the satisfiability of formulas in the language \({\mathfrak L}\) ⋮ A semantic backward chaining proof system ⋮ Semantic trees revisited: Some new completeness results ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ Parsing as non-Horn deduction ⋮ Non-resolution theorem proving ⋮ The search efficiency of theorem proving strategies ⋮ A method for building models automatically. Experiments with an extension of OTTER ⋮ Semantic tableaux with ordering restrictions ⋮ Renamable paramodulation for automatic theorem proving with equality ⋮ Resolution graphs ⋮ Finding resolution proofs and using duplicate goals in AND/OR trees ⋮ Soft typing for ordered resolution ⋮ Theorem proving with variable-constrained resolution ⋮ A note on linear resolution strategies in consequence-finding ⋮ Combining Instance Generation and Resolution ⋮ The \(Q^*\) algorithm - a search strategy for a deductive question-answering system ⋮ Saturation, nonmonotonic reasoning and the closed-world assumption ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ MRPPS?An interactive refutation proof procedure system for question-answering

This page was built for publication: Automatic Theorem Proving With Renamable and Semantic Resolution