Theorema
From MaRDI portal
Software:13705
No author found.
Related Items (only showing first 100 items - show all)
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving ⋮ \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} ⋮ Unnamed Item ⋮ The seventeen provers of the world. Foreword by Dana S. Scott.. ⋮ Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings ⋮ A refinement of de Bruijn's formal language of mathematics ⋮ A fully automatic theorem prover with human-style output ⋮ The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema ⋮ A heuristic prover for elementary analysis in \textit{Theorema} ⋮ Theory exploration powered by deductive synthesis ⋮ Unnamed Item ⋮ Mathematical software -- ICMS 2016. 5th international conference, Berlin, Germany, July 11--14, 2016. Proceedings ⋮ Enabling Symbolic and Numerical Computations in HOL Light ⋮ Automated Reasoning in Reduction Rings Using the Theorema System ⋮ Two-Point Boundary Problems with One Mild Singularity and an Application to Graded Kirchhoff Plates ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Unnamed Item ⋮ Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Gröbner Bases ⋮ Unnamed Item ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ Geometry constructions language ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Formal and efficient primality proofs by use of computer algebra oracles ⋮ Commutative algebra in the Mizar system ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Transforming problems from analysis to algebra: a case study in linear boundary problems ⋮ Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2--6, 2005. Proceedings ⋮ Locking-free compressible quadrilateral finite elements: Poisson's ratio-dependent vector interpolants ⋮ The area method. A recapitulation ⋮ Conjecture synthesis for inductive theories ⋮ Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9--11, 2003. Proceedings ⋮ Unnamed Item ⋮ Formal analysis of optical systems ⋮ 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 ⋮ Synthesis of list algorithms by mechanical proving ⋮ Formalizing polygonal knot origami ⋮ Knowledge-based proof planning ⋮ User interaction with the Matita proof assistant ⋮ Computer algebra in scientific computing. 17th international workshop, CASC 2015, Aachen, Germany, September 14--18, 2015. Proceedings ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ HOL Light QE ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Synthesis of sorting algorithms using multisets in \textit{Theorema} ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Variadic equational matching in associative and commutative theories ⋮ Proof–Based Synthesis of Sorting Algorithms for Trees ⋮ Flat matching ⋮ Mathematical software -- ICMS 2014. 4th international congress, Seoul, South Korea, August 5--9, 2014. Proceedings ⋮ Variadic equational matching ⋮ Towards specifying symbolic computation ⋮ Lemma discovery for induction. A survey ⋮ Designing mathematical libraries based on requirements for theorems ⋮ Mathematical Theory Exploration in Theorema: Reduction Rings ⋮ Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0 ⋮ The GDML and EuKIM Projects: Short Report on the Initiative ⋮ The RISC ProofNavigator: a proving assistant for program verification in the classroom ⋮ Verified interactive computation of definite integrals ⋮ MathLang Translation to Isabelle Syntax ⋮ 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 ⋮ A Symbolic Framework for Operations on Linear Boundary Problems ⋮ Building Mathematics-Based Software Systems to Advance Science and Create Knowledge ⋮ Proof Documents for Automated Origami Theorem Proving ⋮ Thousands of Geometric Problems for Geometric Theorem Provers (TGTP) ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ On the relation between context and sequence unification ⋮ A verified common lisp implementation of Buchberger's algorithm in ACL2 ⋮ Pattern Unification with Sequence Variables and Flexible Arity Symbols ⋮ A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory ⋮ The ForMaRE Project – Formal Mathematical Reasoning in Economics ⋮ The evidence algorithm and problems of representation and processing of mathematical computer knowledge ⋮ Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) ⋮ A machine-checked implementation of Buchberger's algorithm ⋮ GeoThms — a Web System for Euclidean Constructive Geometry ⋮ PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems ⋮ Algorithms and proofs inheritance in the FOC language ⋮ Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema
This page was built for software: Theorema
