The following pages link to (Q4520767):
Displaying 21 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- On theorem prover-based testing (Q470025) (← links)
- Verifying the SET purchase protocols (Q861698) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Integration of formal proof into unified assurance cases with Isabelle/SACM (Q2065527) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743) (← links)
- Proving pointer programs in higher-order logic (Q2486585) (← links)
- A general tableau method for propositional interval temporal logics: theory and implementation (Q2506829) (← links)
- Effective Normalization Techniques for HOL (Q2817937) (← links)
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic (Q2829278) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- The Isabelle Framework (Q3543647) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- A framework for using knowledge in tableau proofs (Q4610337) (← links)
- Sort It Out with Monotonicity (Q5200026) (← links)
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic (Q5504659) (← links)
