The following pages link to (Q3804239):
Displaying 37 items.
- Conjecture synthesis for inductive theories (Q438543) (← links)
- Specifying rewrite strategies for interactive exercises (Q626940) (← links)
- Rippling: A heuristic for guiding inductive proofs (Q685548) (← links)
- Experiments with proof plans for induction (Q809617) (← links)
- On process equivalence = equation solving in CCS (Q839034) (← links)
- Mathematical method and proof (Q857692) (← links)
- Tool-assisted specification and verification of typed low-level languages (Q861687) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Multilanguage hierarchical logics, or: How we can do without modal logics (Q1313954) (← links)
- Using tactics to reformulate formulae for resolution theorem proving (Q1380410) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- Agenda control for heterogeneous reasoners (Q1764797) (← links)
- Constraint solving for proof planning (Q1774557) (← links)
- Proof by analogy in mural (Q1898818) (← links)
- Productive use of failure in inductive proof (Q1915134) (← links)
- Middle-out reasoning for synthesis and induction (Q1915136) (← links)
- Proving theorems by reuse (Q1978233) (← links)
- Knowledge-based proof planning (Q1978469) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- Proof planning with multiple strategies (Q2389631) (← links)
- Crystal: Integrating structured queries into a tactic language (Q2655333) (← links)
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
- Extensions to a generalization critic for inductive proof (Q4647499) (← links)
- Learning Strategies for Mechanised Building of Decision Procedures (Q4916230) (← links)
- PLANS AND PLANNING IN MATHEMATICAL PROOFS (Q5027672) (← links)
- Interleaving Strategies (Q5200118) (← links)
- Synthesis of induction orderings for existence proofs (Q5210760) (← links)
- Reconstructing proofs at the assertion level (Q5210809) (← links)
- Ωmega: Towards a mathematical assistant (Q5234706) (← links)
- Using a generalisation critic to find bisimulations for coinductive proofs (Q5234712) (← links)
- A colored version of the λ-calculus (Q5234713) (← links)
- Mining State-Based Models from Proof Corpora (Q5495930) (← links)
- Higher-order annotated terms for proof search (Q6567727) (← links)
