Theorem-Proving on the Computer

DOI10.1145/321160.321166MaRDI QIDQ3847756zbMATH OpenOpenAlexFDO

Authors John Alan Robinson

Publication date 1963

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/321160.321166

zbMATH Keywords

numerical analysis

Cited in

(20)

• The recursive resolution method for modal logic
• Problem solving by searching for models with a theorem prover
• Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
• An average case analysis of a resolution principle algorithm in mechanical theorem proving.
• The linked conjunct method for automatic deduction and related search techniques
• Editor's introduction to Jean van Heijenoort, ``Historical development of modern logic
• Theorem proving with variable-constrained resolution
• Beweisalgorithmen für die Prädikatenlogik
• A program that computes limits using heuristics to evaluate the indeterminate forms
• Using groups for investigating rewrite systems
• A variant of Herbrand's theorem for formulas in prenex form
• scientific article; zbMATH DE number 3446440 (Why is no real title available?)
• John McCarthy's legacy
• On proof retrieval: Problem-solving machines, I
• Fully reusing clause deduction algorithm based on standard contradiction separation rule
• Computer theorem proving in mathematics
• Circuits, proofs and propositional model counting
• Extending merge resolution to a family of QBF-proof systems
• Refutational theorem proving using term-rewriting systems
• Steps toward a computational metaphysics

This page was built for publication: Theorem-Proving on the Computer

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