An Interactive Driver for Goal-directed Proof Strategies
From MaRDI portal
Publication:5166499
DOI10.1016/J.ENTCS.2008.12.099zbMATH Open1291.68319OpenAlexW2146583274MaRDI QIDQ5166499FDOQ5166499
Authors: Andrea Asperti, Enrico Tassi 
Publication date: 27 June 2014
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.099
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
- User interaction with the Matita proof assistant
- Title not available (Why is that?)
- Types for Proofs and Programs
- Crafting a Proof Assistant
- Linear resolution with selection function
- Title not available (Why is that?)
- The calculus of constructions
- Automation for interactive proof: first prototype
- Automated Reasoning
- Mathematical Knowledge Management
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Working with Mathematical Structures in Type Theory
- A two-level approach towards lean proof-checking
Cited In (7)
- User interaction with the Matita proof assistant
- An interactive derivation viewer
- Click'n prove: interactive proofs within set theory
- Declarative representation of proof terms
- A survey of interactive theorem proving
- Strategic issues, problems and challenges in inductive theorem proving
- The Matita interactive theorem prover
Uses Software
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)
