An Interactive Driver for Goal-directed Proof Strategies

DOI10.1016/J.ENTCS.2008.12.099MaRDI QIDQ5166499zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

automationinteractive theorem provingSLD resolution

Mathematics Subject Classification ID

Logic in computer science (03B70)

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

• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• 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
• 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
• 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

Describes a project that uses

Uses Software

• Whelp
• APT
• Oz Explorer
• CLPGUI
• Matita
• VAMPIRE

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)