An improved proof procedure1
From MaRDI portal
Publication:3279281
DOI10.1111/j.1755-2567.1960.tb00558.xzbMath0099.00801OpenAlexW1968605571MaRDI QIDQ3279281
Publication date: 1960
Published in: Theoria (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1111/j.1755-2567.1960.tb00558.x
Related Items
Unification for infinite sets of equations between finite terms, Seventy Years of Computer Science, Controlled integration of the cut rule into connection tableau calculi, Resolution on formula-trees, History and basic features of the critical-pair/completion procedure, Unification in sort theories and its applications, The disconnection tableau calculus, Unification theory, Liberalized variable splitting, Structured proof procedures, Using rewriting rules for connection graphs to prove theorems, Editor's introduction to Jean van Heijenoort, ``Historical development of modern logic, Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach, My Life as a Logician, What Is Essential Unification?, Minimal model generation with positive unit hyper-resolution tableaux, The Strategy Challenge in SMT Solving, An approach to a systematic theorem proving procedure in first-order logic, An experimental logic based on the fundamental deduction principle, Non-resolution theorem proving, Doing arithmetic without diagrams, Towards the automation of set theory and its logic, What you always wanted to know about rigid E-unification, 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\), Automated theorem proving methods, From Schütte’s Formal Systems to Modern Automated Deduction, Condensed detachment as a rule of inference, Set of support, demodulation, paramodulation: a historical perspective, Group cancellation and resolution
