\textit{Theorema}: Towards computer-aided mathematical theory exploration
type: Item
instance of: scholarly article
title: \textit{Theorema}: Towards computer-aided mathematical theory exploration
zbMATH Open document ID: 1107.68095
author: Bruno Buchberger
author: Adrian Crăciun
author: Tudor Jebelean
author: Laura Kovács
author: Temur Kutsia
author: Koji Nakagawa
author: Florina Piroi
author: Nikolaj Popov
author: Judit Robu
author: Markus Rosenkranz
author: Wolfgang Windsteiger
published in: Journal of Applied Logic
publication date: 2007-02-20T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 13P10
zbMATH DE Number: 5128348
zbMATH Keywords: mathematical assistant
zbMATH Keywords: automated reasoning
zbMATH Keywords: theory exploration
zbMATH Keywords: ``lazy thinking''
describes a project that uses: Coq
describes a project that uses: Waldmeister
describes a project that uses: Bliksem
describes a project that uses: Mathematica
describes a project that uses: SPASS
describes a project that uses: TPTP
describes a project that uses: E Theorem Prover
describes a project that uses: OTTER
describes a project that uses: SETHEO
describes a project that uses: Theorema
describes a project that uses: Nuprl
describes a project that uses: OMDoc
describes a project that uses: LOUI
MaRDI profile type: Publication
full work available at URL: j.jal.2005.10.006
OpenAlex ID: W2133093325
cites work: Mathematical knowledge management in HELM
cites work: Program Development in Computational Logic
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Challenge problems in elementary calculus
cites work: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
cites work: Q3714165
cites work: Q4385444
cites work: Q4394946
cites work: Q4499159
cites work: Q4780208
cites work: Q5699466
cites work: Artificial Intelligence and Symbolic Computation
cites work: Q3021905
cites work: Algorithm synthesis by lazy thinking: examples and implementation in Theorema
cites work: The TH\(\exists\)OREM\(\forall\) project: A progress report
cites work: Q4226993
cites work: Q4377762
cites work: Q5848416
cites work: Q4079605
cites work: Q4144755
cites work: An abstract formalization of correct schemas for program synthesis
cites work: Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
cites work: Decision procedure for indefinite hypergeometric summation
cites work: Productive use of failure in inductive proof
cites work: Q4459895
cites work: Q5781389
cites work: Using Gröbner bases to reason about geometry problems
cites work: Using meta-variables for natural deduction in \textit{Theorema}
cites work: Middle-out reasoning for synthesis and induction
cites work: Q4727657
cites work: Q4447245
cites work: Mathematical Knowledge Management
cites work: On the application of Buchberger's algorithm to automated geometry theorem proving
cites work: SETHEO: A high-performance theorem prover
cites work: Q3995530
cites work: Knowledge-based proof planning
cites work: Q4115244
cites work: A \textit{Mathematica} version of Zeilberger's algorithm for proving binomial coefficient identities
cites work: Q4815329

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Automatic Generation of Polynomial Loop Invariants

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Artificial Intelligence and Symbolic Computation

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: A new symbolic method for solving linear two-point boundary value problems on the level of operators

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Q3150301

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: KI 2004: Advances in Artificial Intelligence

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Q4934624

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Q3853967

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Differentiably finite power series

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: The TPTP problem library. CNF release v1. 2. 1

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Q3685233

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Q4413894

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Q4433984

\textit{Theorema}: Towards computer-aided mathematical theory exploration (cites work)
cites work: Basic principles of mechanical theorem proving in elementary geometries

\textit{Theorema}: Towards computer-aided mathematical theory exploration (DOI)
DOI: 10.1016/J.JAL.2005.10.006