A light-weight integration of automated and interactive theorem proving
From MaRDI portal
Publication:5741559
DOI10.1017/S0960129514000140zbMath1361.68189MaRDI QIDQ5741559
Publication date: 28 July 2016
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Related Items (2)
A sound and complete proof system for a unified temporal logic ⋮ A decision procedure and complete axiomatization for projection temporal logic
Uses Software
Cites Work
- Unnamed Item
- Realizability and intuitionistic logic
- The decision problem for exponential diophantine equations
- Proof reflection in Coq
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Functionality in Combinatory Logic
- Automated Verification of Signalling Principles in Railway Interlocking Systems
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Sledgehammer: Judgement Day
This page was built for publication: A light-weight integration of automated and interactive theorem proving
