A light-weight integration of automated and interactive theorem proving

DOI10.1017/S0960129514000140MaRDI QIDQ5741559zbMATH OpenFDO

Authors Karim Kanso, Anton Setzer

Publication date 28 July 2016

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

Full work available at URL https://doi.org/10.1017/S0960129514000140

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1552511
• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
• Automated Verification of Signalling Principles in Railway Interlocking Systems
• Automated Technology for Verification and Analysis
• Dependently Typed Programming Based on Automated Theorem Proving

Cites work

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

Cited in

(11)

• A decision procedure and complete axiomatization for projection temporal logic
• A sound and complete proof system for a unified temporal logic
• Automation for interactive proof: first prototype
• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
• scientific article; zbMATH DE number 3870635 (Why is no real title available?)
• scientific article; zbMATH DE number 1552511 (Why is no real title available?)
• scientific article; zbMATH DE number 1765687 (Why is no real title available?)
• Integration of automated and interactive theorem proving in ILF
• Automated Technology for Verification and Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Defining trace semantics for CSP-Agda

Describes a project that uses

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)