An improved proof procedure1

Cited in

(33)

Automated theorem proving methods
Condensed detachment as a rule of inference
Resolution on formula-trees
History and basic features of the critical-pair/completion procedure
Unification theory
Using rewriting rules for connection graphs to prove theorems
Non-resolution theorem proving
Doing arithmetic without diagrams
Towards the automation of set theory and its logic
Controlled integration of the cut rule into connection tableau calculi
Unification in sort theories and its applications
Structured proof procedures
Editor's introduction to Jean van Heijenoort, ``Historical development of modern logic
Set of support, demodulation, paramodulation: a historical perspective
Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach
An approach to a systematic theorem proving procedure in first-order logic
Computer proofs of limit theorems
Theorem proving with variable-constrained resolution
Beweisalgorithmen für die Prädikatenlogik
Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
Unification for infinite sets of equations between finite terms
My Life as a Logician
What is essential unification?
Minimal model generation with positive unit hyper-resolution tableaux
The strategy challenge in SMT solving
From Schütte’s Formal Systems to Modern Automated Deduction
Seventy Years of Computer Science
What you always wanted to know about rigid \(E\)-unification
An experimental logic based on the fundamental deduction principle
Artificial intelligence and inherent mathematical difficulty
Group cancellation and resolution
The disconnection tableau calculus
Liberalized variable splitting

This page was built for publication: An improved proof procedure1

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