swMATH961MaRDI QIDQ13705FDOQ13705
Author name not available (Why is that?)
Official website: http://www.risc.jku.at/research/theorema/software/
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
- On the role of OpenMath in interactive mathematical documents
- Title not available (Why is that?)
- \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
- Flat matching
- IsaCoSy
- 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?)
- 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
- 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?)
- 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 symbolic framework for general polynomial domains in Theorema, applications to boundary problems
- 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
- Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
- 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
- A machine-checked implementation of Buchberger's algorithm
- Title not available (Why is that?)
- Pattern unification with sequence variables and flexible arity symbols
- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Towards a symbolic computational philosophy (and methodology!) for mathematics
- Mathematical Knowledge Management
- Automatted geometry theorem proving
- A refinement of de Bruijn's formal language of mathematics
- Synthesis of list algorithms by mechanical proving
- Gröbner bases and systems theory
- A Symbolic Framework for Operations on Linear Boundary Problems
- Finite differences/elements in classical beam problems: Derivation of feasibility conditions under parametric inequality constraints with the help of Reduce and REDLOG
- 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}
- Translating between language and logic: what is easy and what is difficult
- Theory exploration powered by deductive synthesis
- HolPy
- jsCoq
- 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
- Defining power series and polynomials in Mizar
- Title not available (Why is that?)
- Algorithm synthesis by lazy thinking: using problem schemes
- Title not available (Why is that?)
- Title not available (Why is that?)
- Quick specifications for the busy programmer
- The evidence algorithm and problems of representation and processing of mathematical computer knowledge
- Proceedings of the mathematical knowledge management symposium, Edinburgh, UKNEWLINENovember 25--29, 2003
- Reasoning Algebraically About P-Solvable Loops
- User interaction with the Matita proof assistant
- Geometry constructions language
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Mathematica
- MMP/Geometer
- SACLIB
- TkWinHOL
- Xeukleides
- Title not available (Why is that?)
- IsaPlanner
- GEOTHER 1.1
- ALISA
- OMRS
- MetaPRL
- Eukleides
- GeoProof
- Cabri
- GCLCprover
- GeoThms
- Nuprl
- OMDoc
This page was built for software: Theorema
