Theorema
From MaRDI portal
Cited in
(only showing first 100 items - show all)- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs
- Combining logical and algebraic techniques for natural style proving in elementary analysis
- On the relation between context and sequence unification
- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Mathematica
- MMP/Geometer
- jsCoq
- HolPy
- SACLIB
- TkWinHOL
- Xeukleides
- Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9--11, 2003. Proceedings
- IsaPlanner
- GEOTHER 1.1
- ALISA
- The evidence algorithm and problems of representation and processing of mathematical computer knowledge
- OMRS
- A machine-checked implementation of Buchberger's algorithm
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- MetaPRL
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Incorporating quotation and evaluation into Church's type theory
- Eukleides
- GeoProof
- HOL Light QE
- Designing mathematical libraries based on requirements for theorems
- GCLCprover
- GeoThms
- Cabri
- Algorithms and proofs inheritance in the FOC language
- A refinement of de Bruijn's formal language of mathematics
- Nuprl
- OMDoc
- Knowledge-based proof planning
- SgpDec
- Synthesis of sorting algorithms using multisets in \textit{Theorema}
- Variadic equational matching in associative and commutative theories
- CUMODP
- Verified interactive computation of definite integrals
- WinGCLC
- GF
- ForMaRE
- Veriflog
- APS
- IMPS
- Leon
- \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}
- MetaOCaml
- A heuristic prover for elementary analysis in \textit{Theorema}
- LEGO
- CalcCheck
- Minlog
- EgoMath
- SAD
- ForTheL
- IFSGen4LaTeX
- XCentric
- CtCoq
- PhoX
- webDiscovery
- CATIA V5
- PROSPER
- HR
- Analytica
- MathCode
- Variadic equational matching
- Towards specifying symbolic computation
- Lemma discovery for induction. A survey
- Metalibm
- Hipster
- EKHAD
- Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings
- A fully automatic theorem prover with human-style output
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
- Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2--6, 2005. Proceedings
- GeoView
- Locking-free compressible quadrilateral finite elements: Poisson's ratio-dependent vector interpolants
- DSJM
- A new symbolic method for solving linear two-point boundary value problems on the level of operators
- Hidden verification for computational mathematics
- Logicographic symbols
- An automated prover for Zermelo-Fraenkel set theory in Theorema
- Solving equations with sequence variables and sequence functions
- User interaction with the Matita proof assistant
- Mathematical software -- ICMS 2014. 4th international congress, Seoul, South Korea, August 5--9, 2014. Proceedings
- GF
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
- Mathematical software -- ICMS 2016. 5th international conference, Berlin, Germany, July 11--14, 2016. Proceedings
- Geometry constructions language
- A bi-directional extensible interface between Lean and Mathematica
- CodeV
- Zemax
- MathScheme
- LASCAD
- Theorem proving for and with Gröbner bases theory
- SIROCCO
- KeTCindy
- Pycao
- 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
This page was built for software: Theorema
