Theorem Proving via General Matings

Cited in

(66)

Automated theorem proving methods
A decidable fragment of predicate calculus
A Prolog technology theorem prover: Implementation by an extended Prolog compiler
Complexity of resolution proofs and function introduction
A new subsumption method in the connection graph proof procedure
On an unsatisfiability-satisfiability prover
Representing scope in intuitionistic deductions
Universal abstract consistency class and universal refutation
Accelerating tableaux proofs using compact representations
On the termination of clause graph resolution
Embedding complex decision procedures inside an interactive theorem prover.
A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system
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
Higher-order unification revisited: Complete sets of transformations
A comparative study of several proof procedures
Practically useful variants of definitional translations to normal form
TPS: A theorem-proving system for classical type theory
Structured proof procedures
Knowledge-based proof planning
Set of support, demodulation, paramodulation: a historical perspective
Eliminating models during model elimination
Andrews Skolemization may shorten resolution proofs non-elementarily
ABox abduction in the description logic \(\mathcal{ALC}\)
Towards a unified model of search in theorem-proving: subgoal-reduction strategies
nanoCoP: a non-clausal connection prover
Encoding first order proofs in SMT
A Non-clausal Connection Calculus
On the non-confluence of cut-elimination
A proposal for broad spectrum proof certificates
Automating Leibniz's theory of concepts
Protocol Verification Via Rigid/Flexible Resolution
Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
Cyclic connections
Proof-terms for classical and intuitionistic resolution
On the practical value of different definitional translations to normal form
Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
From Schütte’s Formal Systems to Modern Automated Deduction
Efficient ground completion
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
Proving with BDDs and control of information
A practical integration of first-order reasoning and decision procedures
What you always wanted to know about rigid \(E\)-unification
Rigid tree automata and applications
A first polynomial non-clausal class in many-valued logic
Effective Skolemization
Investigations into proof-search in a system of first-order dependent function types
SLIM: An automated reasoner for equivalences, applied to set theory
Higher order E-unification
The TPS theorem proving system
Simultaneous rigid E-unification is undecidable
Combining and automating classical and non-classical logics in classical higher-order logics
The undecidability of simultaneous rigid E-unification
Constraint learning for non-confluent proof search
Theory matrices (for modal logics) using alphabetical monotonicity
A generic deskolemization strategy
Linearity and regularity with negation normal form
Types, Tableaus and Gödel’s God in Isabelle/HOL
Optimizing the clausal normal form transformation
TPS: A hybrid automatic-interactive system for developing proofs
The disconnection tableau calculus
Liberalized variable splitting
On connections and higher-order logic
Rigid E-unification: NP-completeness and applications to equational matings

This page was built for publication: Theorem Proving via General Matings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3906484)