An Interactive Driver for Goal-directed Proof Strategies

DOI10.1016/J.ENTCS.2008.12.099zbMATH Open1291.68319OpenAlexW2146583274MaRDI QIDQ5166499FDOQ5166499

Enrico Tassi, Andrea Asperti

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• User interaction with the Matita proof assistant
• Types for Proofs and Programs
• Crafting a Proof Assistant
• Linear resolution with selection function
• 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 (2)

• Declarative representation of proof terms
• The Matita Interactive Theorem Prover

Uses Software

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

Recommendations

• A synthesis of the procedural and declarative styles of interactive theorem proving 👍 👎
• Goal-directed proof theory 👍 👎
• Towards Ludics Programming: Interactive Proof Search 👍 👎
• Interactive and probabilistic proof-checking 👍 👎
• A Proof-theoretic Analysis of Goal-directed Provability 👍 👎
• A Framework for Interactive Proof 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎

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)