A light-weight integration of automated and interactive theorem proving

DOI10.1017/S0960129514000140zbMATH Open1361.68189MaRDI QIDQ5741559FDOQ5741559

Anton Setzer, Karim Kanso

Publication date: 28 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The decision problem for exponential diophantine equations
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Sledgehammer: Judgement Day
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Automated Verification of Signalling Principles in Railway Interlocking Systems
• Functionality in Combinatory Logic
• Realizability and intuitionistic logic
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Proof reflection in Coq

Cited In (7)

• Title not available (Why is that?)
• Title not available (Why is that?)
• A decision procedure and complete axiomatization for projection temporal logic
• Integration of automated and interactive theorem proving in ILF
• Tools and Algorithms for the Construction and Analysis of Systems
• A sound and complete proof system for a unified temporal logic
• Automation for interactive proof: first prototype

Uses Software

• Agda

This page was built for publication: A light-weight integration of automated and interactive theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5741559)