Theorem Proving via General Matings
From MaRDI portal
Publication:3906484
DOI10.1145/322248.322249zbMath0456.68119OpenAlexW2018221833MaRDI QIDQ3906484
Publication date: 1981
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.466.601
Related Items
Accelerating tableaux proofs using compact representations, On the termination of clause graph resolution, Eliminating models during model elimination, Automating Leibniz’s Theory of Concepts, Efficient ground completion, Embedding complex decision procedures inside an interactive theorem prover., A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation, Andrews Skolemization may shorten resolution proofs non-elementarily, Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system, TPS: A hybrid automatic-interactive system for developing proofs, A Prolog technology theorem prover: Implementation by an extended Prolog compiler, The disconnection tableau calculus, Liberalized variable splitting, TPS: A theorem-proving system for classical type theory, Structured proof procedures, Protocol Verification Via Rigid/Flexible Resolution, A first polynomial non-clausal class in many-valued logic, Effective Skolemization, ABox abduction in the description logic \(\mathcal{ALC}\), On connections and higher-order logic, Rigid E-unification: NP-completeness and applications to equational matings, Combining and automating classical and non-classical logics in classical higher-order logics, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Knowledge-based proof planning, The undecidability of simultaneous rigid E-unification, Proof-terms for classical and intuitionistic resolution, A Non-clausal Connection Calculus, Cyclic connections, Complexity of resolution proofs and function introduction, On the practical value of different definitional translations to normal form, A new subsumption method in the connection graph proof procedure, Theory matrices (for modal logics) using alphabetical monotonicity, Towards Hilbert's 24th Problem: Combinatorial Proof Invariants, Linearity and regularity with negation normal form, Rigid tree automata and applications, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Proving with BDDs and control of information, On the non-confluence of cut-elimination, Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables, On an unsatisfiability-satisfiability prover, nanoCoP: A Non-clausal Connection Prover, Representing scope in intuitionistic deductions, A Proposal for Broad Spectrum Proof Certificates, Higher-order unification revisited: Complete sets of transformations, A practical integration of first-order reasoning and decision procedures, What you always wanted to know about rigid E-unification, Universal abstract consistency class and universal refutation, Decidability and complexity of simultaneous rigid E-unification with one variable and related results, Connection methods in linear logic and proof nets construction, Proof-search in type-theoretic languages: An introduction, A comparative study of several proof procedures, Automated theorem proving methods, Practically useful variants of definitional translations to normal form, From Schütte’s Formal Systems to Modern Automated Deduction, Encoding First Order Proofs in SMT, Set of support, demodulation, paramodulation: a historical perspective, A decidable fragment of predicate calculus, Optimizing the clausal normal form transformation
