Integration of automated and interactive theorem proving in ILF
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1552511
- A light-weight integration of automated and interactive theorem proving
- Automated Reasoning with Analytic Tableaux and Related Methods
- scientific article; zbMATH DE number 3870635
- An integral theorem prover and the role of proof planning
- Interactive theorem proving from the perspective of Isabelle/Isar
- Automated theorem proving and logic programming: a natural symbiosis
- A synthesis of the procedural and declarative styles of interactive theorem proving
Cites work
- \textsf{Ko\(_{\mathsf{M}}\)eT}
- scientific article; zbMATH DE number 1140678 (Why is no real title available?)
- scientific article; zbMATH DE number 827982 (Why is no real title available?)
- Integration of automated and interactive theorem proving in ILF
- Otter 2.0
- SPASS \& FLOTTER version 0.42
- The TPTP problem library
Cited in
(8)- Evaluating general purpose automated theorem proving systems
- Extending Sledgehammer with SMT solvers
- scientific article; zbMATH DE number 500942 (Why is no real title available?)
- Converting non-classical matrix proofs into sequent-style systems
- Integration of automated and interactive theorem proving in ILF
- ILF-SETHEO
- Tools and Algorithms for the Construction and Analysis of Systems
- Controlled use of clausal lemmas in connection tableau calculi
This page was built for publication: Integration of automated and interactive theorem proving in ILF
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5234689)
