\textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646): Difference between revisions

@@ Property / DOI @@
-.1016/j.jal.2005.10.006
@@ Property / DOI: 10.1016/j.jal.2005.10.006 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+OTTER
@@ Property / describes a project that uses: OTTER / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SETHEO
@@ Property / describes a project that uses: SETHEO / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Theorema
@@ Property / describes a project that uses: Theorema / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OMDoc
@@ Property / describes a project that uses: OMDoc / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LOUI
@@ Property / describes a project that uses: LOUI / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.jal.2005.10.006
+Normal rank
@@ Property / OpenAlex ID @@
+W2133093325
@@ Property / OpenAlex ID: W2133093325 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical knowledge management in HELM
@@ Property / cites work: Mathematical knowledge management in HELM / rank @@
+Normal rank
@@ Property / cites work @@
+Program Development in Computational Logic
@@ Property / cites work: Program Development in Computational Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Challenge problems in elementary calculus
@@ Property / cites work: Challenge problems in elementary calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q2902935
@@ Property / cites work: Q2902935 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3714165
@@ Property / cites work: Q3714165 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385444
@@ Property / cites work: Q4385444 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4394946
@@ Property / cites work: Q4394946 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4499159
@@ Property / cites work: Q4499159 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4780208
@@ Property / cites work: Q4780208 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5699466
@@ Property / cites work: Q5699466 / rank @@
+Normal rank
@@ Property / cites work @@
+Artificial Intelligence and Symbolic Computation
@@ Property / cites work: Artificial Intelligence and Symbolic Computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q3021905
@@ Property / cites work: Q3021905 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2847391
@@ Property / cites work: Q2847391 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751543
@@ Property / cites work: Q2751543 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4226993
@@ Property / cites work: Q4226993 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4377762
@@ Property / cites work: Q4377762 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5848416
@@ Property / cites work: Q5848416 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4079605
@@ Property / cites work: Q4079605 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4144755
@@ Property / cites work: Q4144755 / rank @@
+Normal rank
@@ Property / cites work @@
+An abstract formalization of correct schemas for program synthesis
+Normal rank
@@ Property / cites work @@
+Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
+Normal rank
@@ Property / cites work @@
+Decision procedure for indefinite hypergeometric summation
+Normal rank
@@ Property / cites work @@
+Productive use of failure in inductive proof
@@ Property / cites work: Productive use of failure in inductive proof / rank @@
+Normal rank
@@ Property / cites work @@
+Q4459895
@@ Property / cites work: Q4459895 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5781389
@@ Property / cites work: Q5781389 / rank @@
+Normal rank
@@ Property / cites work @@
+Using Gröbner bases to reason about geometry problems
+Normal rank
@@ Property / cites work @@
+Q2751547
@@ Property / cites work: Q2751547 / rank @@
+Normal rank
@@ Property / cites work @@
+Middle-out reasoning for synthesis and induction
@@ Property / cites work: Middle-out reasoning for synthesis and induction / rank @@
+Normal rank
@@ Property / cites work @@
+Q4727657
@@ Property / cites work: Q4727657 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4447245
@@ Property / cites work: Q4447245 / rank @@
+Normal rank
@@ Property / cites work @@
+Artificial Intelligence and Symbolic Computation
@@ Property / cites work: Artificial Intelligence and Symbolic Computation / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+On the application of Buchberger's algorithm to automated geometry theorem proving
+Normal rank
@@ Property / cites work @@
+SETHEO: A high-performance theorem prover
@@ Property / cites work: SETHEO: A high-performance theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q3995530
@@ Property / cites work: Q3995530 / rank @@
+Normal rank
@@ Property / cites work @@
+Knowledge-based proof planning
@@ Property / cites work: Knowledge-based proof planning / rank @@
+Normal rank
@@ Property / cites work @@
+Q4115244
@@ Property / cites work: Q4115244 / rank @@
+Normal rank
@@ Property / cites work @@
+A \textit{Mathematica} version of Zeilberger's algorithm for proving binomial coefficient identities
+Normal rank
@@ Property / cites work @@
+Q4815329
@@ Property / cites work: Q4815329 / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Generation of Polynomial Loop Invariants
+Normal rank
@@ Property / cites work @@
+Artificial Intelligence and Symbolic Computation
@@ Property / cites work: Artificial Intelligence and Symbolic Computation / rank @@
+Normal rank
@@ Property / cites work @@
+A new symbolic method for solving linear two-point boundary value problems on the level of operators
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+KI 2004: Advances in Artificial Intelligence
@@ Property / cites work: KI 2004: Advances in Artificial Intelligence / rank @@
+Normal rank
@@ Property / cites work @@
+Q4934624
@@ Property / cites work: Q4934624 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3853967
@@ Property / cites work: Q3853967 / rank @@
+Normal rank
@@ Property / cites work @@
+Differentiably finite power series
@@ Property / cites work: Differentiably finite power series / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library. CNF release v1. 2. 1
@@ Property / cites work: The TPTP problem library. CNF release v1. 2. 1 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3685233
@@ Property / cites work: Q3685233 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4413894
@@ Property / cites work: Q4413894 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4433984
@@ Property / cites work: Q4433984 / rank @@
+Normal rank
@@ Property / cites work @@
+Basic principles of mechanical theorem proving in elementary geometries
+Normal rank
@@ Property / DOI @@
+.1016/J.JAL.2005.10.006
@@ Property / DOI: 10.1016/J.JAL.2005.10.006 / rank @@
+Normal rank