Theorema

swMATH961MaRDI QIDQ13705FDOQ13705

Author name not available (Why is that?)

Described by source

• Theorema 2.0: A System for Mathematical Theory Exploration
• Groebner Bases in Theorema
• Theorema 2.0: Computer-Assisted Natural-Style Mathematics
• Unnamed Publication

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