Toward Mechanical Mathematics
From MaRDI portal
Cited in
(34)- A decidable fragment of predicate calculus
- On the role of unification in mechanical theorem proving
- Doing arithmetic without diagrams
- Towards the automation of set theory and its logic
- The problem of reasoning by case analysis
- The relative complexity of resolution and cut-free Gentzen systems
- Automated conjecturing. III. Property-relations conjectures
- A method for the synthesis of deducibility conditions for Horn and some other formulas
- lean\(T^ AP\): Lean tableau-based deduction
- Knowledge-based proof planning
- Human-centered automated proof search
- An approach to a systematic theorem proving procedure in first-order logic
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Wanted: collaborative intelligence
- Beweisalgorithmen für die Prädikatenlogik
- Breadth-first search: some surprising results
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
- The reduction method. I:
- Checking proofs
- What is essential unification?
- Canonical Horn representations and query learning
- Construction and learnability of canonical Horn formulas
- Logical approach to control theory and applications
- Glushkov's evidence algorithm
- In Memoriam: Hao Wang 1921–1995
- The strategy challenge in SMT solving
- An introduction to mechanized reasoning
- John McCarthy's legacy
- On Correctness of Mathematical Texts from a Logical and Practical Point of View
- Heuristic programming: A survey
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- Martin Davis: an overview of his work in logic, computer science, and philosophy
- Supporting the formal verification of mathematical texts
- Automated conjecturing. I: Fajtlowicz's Dalmatian heuristic revisited
This page was built for publication: Toward Mechanical Mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3275832)
