CLAM
From MaRDI portal
Cited in
(66)- Automating the synthesis of decision procedures in a constructive metatheory
- Analogy in inductive theorem proving
- Multilanguage hierarchical logics, or: How we can do without modal logics
- A recursion planning analysis of inductive completion
- Using tactics to reformulate formulae for resolution theorem proving
- IsaPlanner
- ALISA
- Proof planning for strategy development
- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
- TAME: Using PVS strategies for special-purpose theorem proving
- Mechanical verification on strategies
- SCR
- Productive use of failure in inductive proof
- Middle-out reasoning for synthesis and induction
- A calculus for and termination of rippling
- Proving theorems by reuse
- TacticToe: learning to prove with tactics
- Amphion
- SPIKE
- Lemma discovery for induction. A survey
- An approach to automatic deductive synthesis of functional programs
- scientific article; zbMATH DE number 1614721 (Why is no real title available?)
- scientific article; zbMATH DE number 1696825 (Why is no real title available?)
- Tactician
- MKRP
- InKa
- Lambda-Clam
- XBarnacle
- OMEGA
- Oyster
- Prodigy
- PROTEIN
- P.rex
- Doris
- Bliksem
- KOMET
- Medmaker
- MATHsAiD
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
- QuodLibet
- GETFOL
- TAME
- CoCLAM
- RRL
- scientific article; zbMATH DE number 1341612 (Why is no real title available?)
- Mollusc
- Extensions to a generalization critic for inductive proof
- Internal analogy in theorem proving
- Termination of algorithms over non-freely generated data types
- Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
- Plans and planning in mathematical proofs
- Termination of constructor systems
- Termination orderings for rippling
- \textit{Mollusc}: a general proof-development shell for sequent-based logics
- Using a generalisation critic to find bisimulations for coinductive proofs
- Reasoning About Incompletely Defined Programs
- KI 2004: Advances in Artificial Intelligence
- Mechanizing Mathematical Reasoning
- Mechanizing Mathematical Reasoning
- Analogy in automated deduction: a survey
- Rippling: A heuristic for guiding inductive proofs
- Experiments with proof plans for induction
- On process equivalence = equation solving in CCS
- An integrated approach to high integrity software verification
- Computer supported mathematics with MEGA
- Supporting the formal verification of mathematical texts
This page was built for software: CLAM
