Theorema
From MaRDI portal
Software:13705
swMATH961MaRDI QIDQ13705FDOQ13705
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Hidden verification for computational mathematics
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Conjecture synthesis for inductive theories
- User interaction with the Matita proof assistant
- On the role of OpenMath in interactive mathematical documents
- Geometry constructions language
- Title not available (Why is that?)
- \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
- Flat matching
- A symbolic framework for general polynomial domains in theorema
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Transforming problems from analysis to algebra: a case study in linear boundary problems
- Locking-free compressible quadrilateral finite elements: Poisson's ratio-dependent vector interpolants
- The TH\(\exists\)OREM\(\forall\) project: A progress report
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
- Algorithm synthesis by lazy thinking: examples and implementation in Theorema
- Automated Deduction in Geometry
- Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Gröbner Bases
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proof Documents for Automated Origami Theorem Proving
- Mathematical Knowledge Management
- A fully automatic theorem prover with human-style output
- Title not available (Why is that?)
- Towards a Symbolic Computational Philosophy (and Methodology!) for Mathematics
- The area method. A recapitulation
- Commutative algebra in the Mizar system
- Formal and efficient primality proofs by use of computer algebra oracles
- Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9--11, 2003. Proceedings
- Formalizing polygonal knot origami
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2--6, 2005. Proceedings
- Title not available (Why is that?)
- A new symbolic method for solving linear two-point boundary value problems on the level of operators
- Formal analysis of optical systems
- Computer algebra in scientific computing. 17th international workshop, CASC 2015, Aachen, Germany, September 14--18, 2015. Proceedings
- On the relation between context and sequence unification
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- Title not available (Why is that?)
- Knowledge-based proof planning
- On Correctness of Mathematical Texts from a Logical and Practical Point of View
- Combining logical and algebraic techniques for natural style proving in elementary analysis
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs
- Verified interactive computation of definite integrals
- Mathematical Knowledge Management
- HOL Light QE
- A machine-checked implementation of Buchberger's algorithm
- Title not available (Why is that?)
- Hipster: Integrating Theory Exploration in a Proof Assistant
- Mathematical Knowledge Management
- Mathematical software -- ICMS 2016. 5th international conference, Berlin, Germany, July 11--14, 2016. Proceedings
- A refinement of de Bruijn's formal language of mathematics
- Synthesis of list algorithms by mechanical proving
- Gröbner bases and systems theory
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
- A Symbolic Framework for Operations on Linear Boundary Problems
- SAD as a mathematical assistant -- how should we go from here to there?
- Symbolic computation and automated reasoning. The CALCULEMUS-2000 symposium. 8th symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, GB, August 6--7, 2000
- Using meta-variables for natural deduction in \textit{Theorema}
- Theory exploration powered by deductive synthesis
- Towards specifying symbolic computation
- Computer aided systems theory - EUROCAST 2001. A selection of papers from the 8th international workshop, Las Palmas de Gran Canaria, Spain, February 19--23, 2001. Revised papers
- Solving equations with sequence variables and sequence functions
- Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
- GeoThms -- a web system for Euclidean constructive geometry
- GCLC -- a tool for constructive Euclidean geometry and more than that
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Defining power series and polynomials in Mizar
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Thousands of geometric problems for geometric theorem provers (TGTP)
- Title not available (Why is that?)
- Algorithm synthesis by lazy thinking: using problem schemes
- Title not available (Why is that?)
- Quick specifications for the busy programmer
- Reasoning Algebraically About P-Solvable Loops
- A new symbolic method for linear boundary value problems using Groebner bases
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
- Synthesis of sorting algorithms using multisets in \textit{Theorema}
- Title not available (Why is that?)
- Two-Point Boundary Problems with One Mild Singularity and an Application to Graded Kirchhoff Plates
- Algorithms and proofs inheritance in the FOC language
- MathLang Translation to Isabelle Syntax
- Title not available (Why is that?)
- \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}
- Communicating mathematics in the digital era (CMDE 2006). Selected papers based on the presentations at the meeting (CMDE 2006), Aveiro, Portugal, August 15--18, 2006.
- Generation and presentation of formal mathematical documents
- Logicographic symbols
- A formal framework for managing mathematics
- Mathematical knowledge management using theorema
- Title not available (Why is that?)
- Title not available (Why is that?)
- A heuristic prover for elementary analysis in \textit{Theorema}
- Two tools for mathematical knowledge management in theorema
This page was built for software: Theorema