An Interactive Driver for Goal-directed Proof Strategies

DOI10.1016/j.entcs.2008.12.099zbMath1291.68319OpenAlexW2146583274MaRDI QIDQ5166499

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

Related Items (2)

Declarative representation of proof terms ⋮ The Matita Interactive Theorem Prover

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Automation for interactive proof: first prototype
• User interaction with the Matita proof assistant
• Linear resolution with selection function
• Working with Mathematical Structures in Type Theory
• Crafting a Proof Assistant
• A two-level approach towards lean proof-checking
• Automated Reasoning
• Mathematical Knowledge Management
• Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
• Types for Proofs and Programs

This page was built for publication: An Interactive Driver for Goal-directed Proof Strategies