Pages that link to "Item:Q865646"
From MaRDI portal
The following pages link to \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646):
Displaying 31 items.
- The area method. A recapitulation (Q437042) (← links)
- Conjecture synthesis for inductive theories (Q438543) (← links)
- Formal analysis of optical systems (Q475384) (← links)
- Synthesis of list algorithms by mechanical proving (Q485837) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Flat matching (Q999086) (← links)
- The RISC ProofNavigator: a proving assistant for program verification in the classroom (Q1019024) (← links)
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs (Q1025311) (← links)
- On the relation between context and sequence unification (Q1034550) (← links)
- A verified common lisp implementation of Buchberger's algorithm in ACL2 (Q1034553) (← links)
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (Q1687709) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Variadic equational matching in associative and commutative theories (Q2029000) (← links)
- A fully automatic theorem prover with human-style output (Q2362206) (← links)
- User interaction with the Matita proof assistant (Q2462635) (← links)
- Geometry constructions language (Q2655329) (← links)
- GeoThms — a Web System for Euclidean Constructive Geometry (Q2867934) (← links)
- Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery (Q3058453) (← links)
- Thousands of Geometric Problems for Geometric Theorem Provers (TGTP) (Q3102742) (← links)
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs (Q3102745) (← links)
- MathLang Translation to Isabelle Syntax (Q3637293) (← links)
- A Symbolic Framework for Operations on Linear Boundary Problems (Q3644106) (← links)
- Translating between Language and Logic: What Is Easy and What Is Difficult (Q5200012) (← links)
- Using Theorema in the Formalization of Theoretical Economics (Q5200108) (← links)
- Quick specifications for the busy programmer (Q5371995) (← links)
- Automatic Verification of Regular Constructions in Dynamic Geometry Systems (Q5453483) (← links)
- Reasoning Algebraically About P-Solvable Loops (Q5458331) (← links)
- Hipster: Integrating Theory Exploration in a Proof Assistant (Q5495917) (← links)
- High-Level Theories (Q5505502) (← links)
- On Correctness of Mathematical Texts from a Logical and Practical Point of View (Q5505538) (← links)
- Automated theorem proving in the classroom (Q6653958) (← links)
