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

DOI10.1007/978-3-030-81097-9_10MaRDI QIDQ2128808zbMATH OpenOpenAlexFDO

Authors 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

computer algebranatural-style proofssatisfiability checkingsatisfiability modulo theoriessymbolic computation

Mathematics Subject Classification ID

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) Symbolic computation and algebraic computation (68W30)

Recommendations

• Combining logical and algebraic techniques for natural style proving in elementary analysis
• scientific article; zbMATH DE number 2065273
• Analytica --- an experiment in combining theorem proving and symbolic computation
• MetiTarski: An Automatic Prover for the Elementary Functions
• MetiTarski: An automatic theorem prover for real-valued special functions

Cites work

• Analytica --- an experiment in combining theorem proving and symbolic computation
• Combining logical and algebraic techniques for natural style proving in elementary analysis
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• Theorema 2.0: computer-assisted natural-style mathematics

Cited in

(10)

• Combining logical and algebraic techniques for natural style proving in elementary analysis
• Analytica --- an experiment in combining theorem proving and symbolic computation
• An interactive calculus theorem-prover for continuity properties
• A heuristic prover for real inequalities
• scientific article; zbMATH DE number 1222425 (Why is no real title available?)
• scientific article; zbMATH DE number 2000433 (Why is no real title available?)
• scientific article; zbMATH DE number 2065273 (Why is no real title available?)
• Formalization techniques for asymptotic reasoning in classical analysis
• Experiments with automated reasoning in the class
• Analytica -- an experiment in combining theorem proving and symbolic computation

Describes a project that uses

Uses Software

• Theorema
• Analytica

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

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