scientific article; zbMATH DE number 4072439
From MaRDI portal
Publication:3804239
Recommendations
Cited in
(42)- Multilanguage hierarchical logics, or: How we can do without modal logics
- Using tactics to reformulate formulae for resolution theorem proving
- Proof-search in type-theoretic languages: An introduction
- Formalization of the resolution calculus for first-order logic
- Agenda control for heterogeneous reasoners
- Constraint solving for proof planning
- Proof by analogy in mural
- Productive use of failure in inductive proof
- Middle-out reasoning for synthesis and induction
- Proving theorems by reuse
- Knowledge-based proof planning
- TacticToe: learning to prove with tactics
- Towards finding longer proofs
- Proof planning with multiple strategies
- Crystal: Integrating structured queries into a tactic language
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Conjecture synthesis for inductive theories
- Extensions to a generalization critic for inductive proof
- Learning strategies for mechanised building of decision procedures
- Plans and planning in mathematical proofs
- Interleaving strategies
- Synthesis of induction orderings for existence proofs
- Reconstructing proofs at the assertion level
- \(\Omega\)\textsc{mega}: towards a mathematical assistant
- Using a generalisation critic to find bisimulations for coinductive proofs
- A colored version of the -calculus
- Mining state-based models from proof corpora
- Specifying rewrite strategies for interactive exercises
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Extensions to the rippling-out tactic for guiding inductive proofs
- Guiding induction proofs
- A science of reasoning: Extended abstract
- Higher-order annotated terms for proof search
- Rippling: A heuristic for guiding inductive proofs
- The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
- Experiments with proof plans for induction
- On process equivalence = equation solving in CCS
- Mathematical method and proof
- Tool-assisted specification and verification of typed low-level languages
- A proof-centric approach to mathematical assistants
- Computer supported mathematics with MEGA
- Supporting the formal verification of mathematical texts
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3804239)
