The following pages link to Theorema (Q13705):
Displaying 50 items.
- Transforming problems from analysis to algebra: a case study in linear boundary problems (Q413404) (← links)
- The area method. A recapitulation (Q437042) (← links)
- Conjecture synthesis for inductive theories (Q438543) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- Synthesis of list algorithms by mechanical proving (Q485837) (← links)
- Formalizing polygonal knot origami (Q485841) (← links)
- Computer algebra in scientific computing. 17th international workshop, CASC 2015, Aachen, Germany, September 14--18, 2015. Proceedings (Q499580) (← links)
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings (Q555659) (← links)
- Formal and efficient primality proofs by use of computer algebra oracles (Q597112) (← links)
- Commutative algebra in the Mizar system (Q597122) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Flat matching (Q999086) (← links)
- The RISC ProofNavigator: a proving assistant for program verification in the classroom (Q1019024) (← links)
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs (Q1025311) (← links)
- Combining logical and algebraic techniques for natural style proving in elementary analysis (Q1025313) (← links)
- On the relation between context and sequence unification (Q1034550) (← links)
- A verified common lisp implementation of Buchberger's algorithm in ACL2 (Q1034553) (← links)
- Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9--11, 2003. Proceedings (Q1418343) (← links)
- The evidence algorithm and problems of representation and processing of mathematical computer knowledge (Q1582906) (← links)
- A machine-checked implementation of Buchberger's algorithm (Q1595926) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (Q1687709) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- HOL Light QE (Q1791161) (← links)
- Designing mathematical libraries based on requirements for theorems (Q1810919) (← links)
- Algorithms and proofs inheritance in the FOC language (Q1868513) (← links)
- A refinement of de Bruijn's formal language of mathematics (Q1876109) (← links)
- Knowledge-based proof planning (Q1978469) (← links)
- Synthesis of sorting algorithms using multisets in \textit{Theorema} (Q1996870) (← links)
- Variadic equational matching in associative and commutative theories (Q2029000) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} (Q2119984) (← links)
- A heuristic prover for elementary analysis in \textit{Theorema} (Q2128808) (← links)
- Variadic equational matching (Q2287900) (← links)
- Towards specifying symbolic computation (Q2287903) (← links)
- Lemma discovery for induction. A survey (Q2287904) (← links)
- Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings (Q2359450) (← links)
- A fully automatic theorem prover with human-style output (Q2362206) (← links)
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (Q2364696) (← links)
- Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2--6, 2005. Proceedings (Q2425579) (← links)
- Locking-free compressible quadrilateral finite elements: Poisson's ratio-dependent vector interpolants (Q2435352) (← links)
- A new symbolic method for solving linear two-point boundary value problems on the level of operators (Q2456540) (← links)
- Hidden verification for computational mathematics (Q2456559) (← links)
- Logicographic symbols (Q2457342) (← links)
- An automated prover for Zermelo-Fraenkel set theory in Theorema (Q2457343) (← links)
- Solving equations with sequence variables and sequence functions (Q2457427) (← links)
- User interaction with the Matita proof assistant (Q2462635) (← links)
