scientific article
From MaRDI portal
Publication:3954845
zbMath0492.68067MaRDI QIDQ3954845
Publication date: 1982
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)
Related Items
TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic ⋮ Problem solving by searching for models with a theorem prover ⋮ Eliminating models during model elimination ⋮ History and Prospects for First-Order Automated Deduction ⋮ Resolution on formula-trees ⋮ \(M\)-calculus -- a sequent method for automatic theorem proving ⋮ The model evolution calculus as a first-order DPLL method ⋮ A Prolog technology theorem prover: Implementation by an extended Prolog compiler ⋮ Craig interpolation with clausal first-order tableaux ⋮ A logic-based model of intention formation and action for multi-agent subcontracting ⋮ Cyclic connections ⋮ Situational Calculus, linear connection proofs and STRIPS-like planning: An experimental comparison ⋮ Complexity of resolution proofs and function introduction ⋮ An automatic proof of Gödel's incompleteness theorem ⋮ The relative complexity of analytic tableaux and SL-resolution ⋮ Connection calculus theorem proving with multiple built-in theories ⋮ A deductive solution for plan generation ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures ⋮ Representing scope in intuitionistic deductions ⋮ Syntactical treatments of propositional attitudes ⋮ A practical integration of first-order reasoning and decision procedures ⋮ A comparative study of several proof procedures ⋮ Automated theorem proving methods ⋮ Gentzen-type systems, resolution and tableaux ⋮ Optimizing the clausal normal form transformation ⋮ Automated inferencing ⋮ Properties of substitutions and unifications
This page was built for publication:
