\textit{Theorema}: Towards computer-aided mathematical theory exploration
From MaRDI portal
Publication:865646
DOI10.1016/J.JAL.2005.10.006zbMath1107.68095OpenAlexW2133093325MaRDI QIDQ865646
Koji Nakagawa, Bruno Buchberger, Florina Piroi, Wolfgang Windsteiger, Tudor Jebelean, Adrian Crǎciun, Markus Rosenkranz, Judit Robu, Laura Kovács, Nikolaj Popov, Temur Kutsia
Publication date: 20 February 2007
Published in: Journal of Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.006
Related Items (31)
A fully automatic theorem prover with human-style output ⋮ Theory exploration powered by deductive synthesis ⋮ Geometry constructions language ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Learning to reason assisted by automated reasoning ⋮ The area method. A recapitulation ⋮ Conjecture synthesis for inductive theories ⋮ Quick specifications for the busy programmer ⋮ Formal analysis of optical systems ⋮ Synthesis of list algorithms by mechanical proving ⋮ User interaction with the Matita proof assistant ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Variadic equational matching in associative and commutative theories ⋮ Translating between Language and Logic: What Is Easy and What Is Difficult ⋮ Using Theorema in the Formalization of Theoretical Economics ⋮ Flat matching ⋮ Automatic Verification of Regular Constructions in Dynamic Geometry Systems ⋮ Reasoning Algebraically About P-Solvable Loops ⋮ The RISC ProofNavigator: a proving assistant for program verification in the classroom ⋮ MathLang Translation to Isabelle Syntax ⋮ Using computer algebra techniques for the specification, verification and synthesis of recursive programs ⋮ A Symbolic Framework for Operations on Linear Boundary Problems ⋮ Thousands of Geometric Problems for Geometric Theorem Provers (TGTP) ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ On the relation between context and sequence unification ⋮ A verified common lisp implementation of Buchberger's algorithm in ACL2 ⋮ Hipster: Integrating Theory Exploration in a Proof Assistant ⋮ High-Level Theories ⋮ On Correctness of Mathematical Texts from a Logical and Practical Point of View ⋮ GeoThms — a Web System for Euclidean Constructive Geometry
Uses Software
Cites Work
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Challenge problems in elementary calculus
- On the application of Buchberger's algorithm to automated geometry theorem proving
- Using Gröbner bases to reason about geometry problems
- Basic principles of mechanical theorem proving in elementary geometries
- Differentiably finite power series
- SETHEO: A high-performance theorem prover
- The TPTP problem library. CNF release v1. 2. 1
- Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
- An abstract formalization of correct schemas for program synthesis
- Mathematical knowledge management in HELM
- Productive use of failure in inductive proof
- Middle-out reasoning for synthesis and induction
- A \textit{Mathematica} version of Zeilberger's algorithm for proving binomial coefficient identities
- Knowledge-based proof planning
- A new symbolic method for solving linear two-point boundary value problems on the level of operators
- Decision procedure for indefinite hypergeometric summation
- Automatic Generation of Polynomial Loop Invariants
- Mathematical Knowledge Management
- KI 2004: Advances in Artificial Intelligence
- Artificial Intelligence and Symbolic Computation
- Artificial Intelligence and Symbolic Computation
- Artificial Intelligence and Symbolic Computation
- Program Development in Computational Logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: \textit{Theorema}: Towards computer-aided mathematical theory exploration
