scientific article; zbMATH DE number 194631

Publication date: 5 June 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

bibliography resolution automated theorem proving classical logic connection method connection calculus deduction reasoning inferential strategies

Mathematics Subject Classification ID

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

Practical Proof Search for Coq by Type Inhabitation, Prolog Technology Reinforcement Learning Prover, Controlled integration of the cut rule into connection tableau calculi, The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics, A new methodology for query answering in default logics via structure-oriented theorem proving, KoMeT, Constraint satisfaction from a deductive viewpoint, TPS: A hybrid automatic-interactive system for developing proofs, Increasing the efficiency of automated theorem proving, The disconnection tableau calculus, Liberalized variable splitting, TPS: A theorem-proving system for classical type theory, IeanCOP: lean connection-based theorem proving, Incremental variable splitting, Lean induction principles for tableaux, Hintikka multiplicities in matrix decision methods for some propositional modal logics, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions), Skeptical query-answering in Constrained Default Logic, Hilbert's epsilon as an operator of indefinite committed choice, A Non-clausal Connection Calculus, Incremental theory reasoning methods for semantic tableaux, The disconnection method, T-string unification: Unifying prefixes in non-classical proof methods, A semantic backward chaining proof system, XRay: A prolog technology theorem prover for default reasoning: A system description, On the practical value of different definitional translations to normal form, Converting non-classical matrix proofs into sequent-style systems, Theory matrices (for modal logics) using alphabetical monotonicity, Parsing as non-Horn deduction, Proof Search for the First-Order Connection Calculus in Maude, Machine learning guidance for connection tableaux, The search efficiency of theorem proving strategies, Model elimination without contrapositives, Detecting non-provable goals, Proving with BDDs and control of information, Semantic tableaux with ordering restrictions, A Connection Calculus for the Description Logic $$ {\mathcal{ALC}} $$, nanoCoP: A Non-clausal Connection Prover, Let's plan it deductively!, Prolog technology for default reasoning: proof theory and compilation techniques, Connection-based proof construction in linear logic, A query answering algorithm for Lukaszewicz' general open default theory, Solution lifting method for handling meta-variables in TH$\exists$OREM$\forall$, A uniform procedure for converting matrix proofs into sequent-style systems, From Schütte’s Formal Systems to Modern Automated Deduction, Set of support, demodulation, paramodulation: a historical perspective, Simplification in a satisfiability checker for VLSI applications, Hypothesis finding with proof theoretical appropriateness criteria

Uses Software

PRV