\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
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
