Pages that link to "Item:Q3906484"
From MaRDI portal
The following pages link to Theorem Proving via General Matings (Q3906484):
Displayed 50 items.
- Rigid tree automata and applications (Q553317) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- The undecidability of simultaneous rigid E-unification (Q671659) (← links)
- Theory matrices (for modal logics) using alphabetical monotonicity (Q687154) (← links)
- Linearity and regularity with negation normal form (Q703486) (← links)
- Optimizing the clausal normal form transformation (Q809622) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Liberalized variable splitting (Q877894) (← links)
- On connections and higher-order logic (Q908896) (← links)
- Rigid E-unification: NP-completeness and applications to equational matings (Q921913) (← links)
- Automated theorem proving methods (Q1057850) (← links)
- A decidable fragment of predicate calculus (Q1066880) (← links)
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler (Q1114446) (← links)
- Complexity of resolution proofs and function introduction (Q1194246) (← links)
- A new subsumption method in the connection graph proof procedure (Q1199542) (← links)
- On an unsatisfiability-satisfiability prover (Q1264000) (← links)
- Representing scope in intuitionistic deductions (Q1274448) (← links)
- Universal abstract consistency class and universal refutation (Q1288438) (← links)
- Accelerating tableaux proofs using compact representations (Q1334905) (← links)
- On the termination of clause graph resolution (Q1344889) (← links)
- Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) (← links)
- A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation (Q1354059) (← links)
- Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system (Q1364068) (← links)
- Decidability and complexity of simultaneous rigid E-unification with one variable and related results (Q1575636) (← links)
- Connection methods in linear logic and proof nets construction (Q1575926) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
- A comparative study of several proof procedures (Q1836483) (← links)
- Practically useful variants of definitional translations to normal form (Q1854384) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Structured proof procedures (Q1924823) (← links)
- Knowledge-based proof planning (Q1978469) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Eliminating models during model elimination (Q2142079) (← links)
- Andrews Skolemization may shorten resolution proofs non-elementarily (Q2151391) (← links)
- ABox abduction in the description logic \(\mathcal{ALC}\) (Q2429984) (← links)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
- nanoCoP: A Non-clausal Connection Prover (Q2817929) (← links)
- Encoding First Order Proofs in SMT (Q2864408) (← links)
- A Non-clausal Connection Calculus (Q3010371) (← links)
- On the non-confluence of cut-elimination (Q3083141) (← links)
- A Proposal for Broad Spectrum Proof Certificates (Q3100201) (← links)
- Automating Leibniz’s Theory of Concepts (Q3454082) (← links)
- Protocol Verification Via Rigid/Flexible Resolution (Q3498469) (← links)
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables (Q3631368) (← links)
- Cyclic connections (Q4645228) (← links)
- Proof-terms for classical and intuitionistic resolution (Q4647497) (← links)
- On the practical value of different definitional translations to normal form (Q4647537) (← links)
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants (Q4917988) (← links)