The following pages link to An improved proof procedure1 (Q3279281):
Displaying 32 items.
- Unification for infinite sets of equations between finite terms (Q287056) (← links)
- An experimental logic based on the fundamental deduction principle (Q580998) (← links)
- Group cancellation and resolution (Q817703) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- Liberalized variable splitting (Q877894) (← links)
- Automated theorem proving methods (Q1057850) (← links)
- Condensed detachment as a rule of inference (Q1060210) (← links)
- Resolution on formula-trees (Q1098648) (← links)
- History and basic features of the critical-pair/completion procedure (Q1103414) (← links)
- Unification theory (Q1124375) (← links)
- Using rewriting rules for connection graphs to prove theorems (Q1137877) (← links)
- Non-resolution theorem proving (Q1238434) (← links)
- Doing arithmetic without diagrams (Q1238641) (← links)
- Towards the automation of set theory and its logic (Q1253108) (← links)
- Controlled integration of the cut rule into connection tableau calculi (Q1344875) (← links)
- Unification in sort theories and its applications (Q1380412) (← links)
- Structured proof procedures (Q1924823) (← links)
- Editor's introduction to Jean van Heijenoort, ``Historical development of modern logic'' (Q1942090) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach (Q2219192) (← links)
- An approach to a systematic theorem proving procedure in first-order logic (Q2264551) (← links)
- Computer proofs of limit theorems (Q2554244) (← links)
- Theorem proving with variable-constrained resolution (Q2554609) (← links)
- Beweisalgorithmen für die Prädikatenlogik (Q2558006) (← links)
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) (Q2577589) (← links)
- My Life as a Logician (Q3305314) (← links)
- What Is Essential Unification? (Q3305325) (← links)
- Minimal model generation with positive unit hyper-resolution tableaux (Q4645233) (← links)
- The Strategy Challenge in SMT Solving (Q4913859) (← links)
- From Schütte’s Formal Systems to Modern Automated Deduction (Q5013905) (← links)
- Seventy Years of Computer Science (Q5049043) (← links)
- What you always wanted to know about rigid E-unification (Q5235253) (← links)
