A Proof Method for Quantification Theory: Its Justification and Realization

DOI10.1147/rd.41.0028zbMath0097.00301OpenAlexW2069224897WikidataQ56038649 ScholiaQ56038649MaRDI QIDQ3275827

Paul C. Gilmore

Publication date: 1960

Published in: IBM Journal of Research and Development (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1147/rd.41.0028

zbMATH Keywords

philosophy and foundations of mathematics

Related Items

History and Prospects for First-Order Automated Deduction, Structured proof procedures, Unnamed Item, The \(Multi\)-SAT algorithm, What Is Essential Unification?, DPLL: The Core of Modern Satisfiability Solvers, The Strategy Challenge in SMT Solving, John McCarthy's legacy, On the role of unification in mechanical theorem proving, Semantically guided first-order theorem proving using hyper-linking, An examination of the geometry theorem machine, Theorem proving with variable-constrained resolution, Beweisalgorithmen für die Prädikatenlogik, First order Stålmarck. Universal lemmas through branch merges, On proof retrieval: Problem-solving machines, I, Automated theorem proving methods, Wanted: collaborative intelligence, A posthumous contribution by Larry Wos: excerpts from an unpublished column, La théorie des fonctions récursives et ses applications. (Exposé d'information générale), Group cancellation and resolution