Toward Mechanical Mathematics

DOI10.1147/rd.41.0002zbMath0097.00404OpenAlexW2085089824WikidataQ56454837 ScholiaQ56454837MaRDI QIDQ3275832

Hao Wang

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.0002

zbMATH Keywords

philosophy and foundations of mathematics

Related Items (33)

The relative complexity of resolution and cut-free Gentzen systems ⋮ lean\(T^ AP\): Lean tableau-based deduction ⋮ Supporting the formal verification of mathematical texts ⋮ Checking Proofs ⋮ Automated conjecturing. III. Property-relations conjectures ⋮ Heuristic programming: A survey ⋮ Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ Construction and learnability of canonical Horn formulas ⋮ Automated conjecturing. I: Fajtlowicz's Dalmatian heuristic revisited ⋮ In Memoriam: Hao Wang 1921–1995 ⋮ Glushkov's evidence algorithm ⋮ Knowledge-based proof planning ⋮ What Is Essential Unification? ⋮ Logical approach to control theory and applications ⋮ An introduction to mechanized reasoning ⋮ The Strategy Challenge in SMT Solving ⋮ John McCarthy's legacy ⋮ An approach to a systematic theorem proving procedure in first-order logic ⋮ On the role of unification in mechanical theorem proving ⋮ Doing arithmetic without diagrams ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Towards the automation of set theory and its logic ⋮ Canonical Horn Representations and Query Learning ⋮ Human-centered automated proof search ⋮ Beweisalgorithmen für die Prädikatenlogik ⋮ Breadth-first search: some surprising results ⋮ On Correctness of Mathematical Texts from a Logical and Practical Point of View ⋮ A method for the synthesis of deducibility conditions for Horn and some other formulas ⋮ Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) ⋮ The reduction method. I: ⋮ Wanted: collaborative intelligence ⋮ A decidable fragment of predicate calculus ⋮ The problem of reasoning by case analysis

This page was built for publication: Toward Mechanical Mathematics