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

DOI10.1007/978-3-030-81097-9_10zbMATH Open1485.68284OpenAlexW3174333326MaRDI QIDQ2128808FDOQ2128808

Tudor Jebelean

Publication date: 22 April 2022

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

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

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)

Cites Work

• Theorema 2.0: Computer-Assisted Natural-Style Mathematics
• Title not available (Why is that?)
• Combining logical and algebraic techniques for natural style proving in elementary analysis
• Analytica --- an experiment in combining theorem proving and symbolic computation

Cited In (4)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Experiments with automated reasoning in the class
• An interactive calculus theorem-prover for continuity properties

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)