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 algebrasymbolic computationsatisfiability modulo theoriessatisfiability checkingnatural-style proofs

Mathematics Subject Classification ID

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

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

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

Cited in

(8)

• A heuristic prover for real inequalities
• Combining logical and algebraic techniques for natural style proving in elementary analysis
• Experiments with automated reasoning in the class
• scientific article; zbMATH DE number 2000433 (Why is no real title available?)
• Formalization techniques for asymptotic reasoning in classical analysis
• An interactive calculus theorem-prover for continuity properties
• scientific article; zbMATH DE number 2065273 (Why is no real title available?)
• 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)