An Interactive Driver for Goal-directed Proof Strategies
From MaRDI portal
Recommendations
- A Proof-theoretic Analysis of Goal-directed Provability
- A Framework for Interactive Proof
- scientific article; zbMATH DE number 1629956
- Goal-directed proof theory
- Towards Ludics Programming: Interactive Proof Search
- scientific article; zbMATH DE number 3870635
- A survey of interactive theorem proving
- scientific article; zbMATH DE number 1696800
- Interactive and probabilistic proof-checking
- A synthesis of the procedural and declarative styles of interactive theorem proving
Cites work
- A two-level approach towards lean proof-checking
- Automated Reasoning
- Automation for interactive proof: first prototype
- Crafting a Proof Assistant
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 43398 (Why is no real title available?)
- Linear resolution with selection function
- Mathematical Knowledge Management
- The calculus of constructions
- Types for Proofs and Programs
- User interaction with the Matita proof assistant
- Working with Mathematical Structures in Type Theory
Cited in
(7)- User interaction with the Matita proof assistant
- Declarative representation of proof terms
- Strategic issues, problems and challenges in inductive theorem proving
- An interactive derivation viewer
- Click'n prove: interactive proofs within set theory
- The Matita interactive theorem prover
- A survey of interactive theorem proving
This page was built for publication: An Interactive Driver for Goal-directed Proof Strategies
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5166499)
