A heuristic prover for elementary analysis in \textit{Theorema}

DOI10.1007/978-3-030-81097-9_10zbMath1485.68284OpenAlexW3174333326MaRDI QIDQ2128808

Tudor Jebelean

Publication date: 22 April 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81097-9_10

zbMATH Keywords

symbolic computationcomputer algebrasatisfiability modulo theoriessatisfiability checkingnatural-style proofs

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to real functions (26-01) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Experiments with automated reasoning in the class

Uses Software

• Theorema
• Analytica

Cites Work

• Unnamed Item
• Combining logical and algebraic techniques for natural style proving in elementary analysis
• Analytica --- an experiment in combining theorem proving and symbolic computation
• Theorema 2.0: Computer-Assisted Natural-Style Mathematics

This page was built for publication: A heuristic prover for elementary analysis in \textit{Theorema}