A light-weight integration of automated and interactive theorem proving

DOI10.1017/S0960129514000140zbMATH Open1361.68189MaRDI QIDQ5741559FDOQ5741559

Authors: Karim Kanso, Anton Setzer 

Publication date: 28 July 2016

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

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

Mathematics Subject Classification ID

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Title not available (Why is that?)
• 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 (10)

• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
• Title not available (Why is that?)
• 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
• Automated Technology for Verification and Analysis
• 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)