The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
type: Item
instance of: scholarly article
title: The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
zbMATH Open document ID: 1216.68233
author: Michael J. C. Gordon
author: Matt Kaufmann
author: Sandip Ray
published in: Journal of Automated Reasoning
publication date: 2011-06-03T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5903837
zbMATH Keywords: theorem proving
zbMATH Keywords: automated reasoning
zbMATH Keywords: higher-order logic
zbMATH Keywords: combining theorem provers
zbMATH Keywords: linear temporal logic
zbMATH Keywords: model checking
describes a project that uses: ACL2
describes a project that uses: SPIN
describes a project that uses: HOL
describes a project that uses: ML
MaRDI profile type: Publication
full work available at URL: s10817-010-9169-y
OpenAlex ID: W2003674078
cites work: Q5287513
cites work: Q4809048
cites work: Logic in Computer Science
cites work: Structured theory development for a mechanized logic
cites work: An ACL2 Tutorial
cites work: Q4326390
cites work: Executable JVM model for analytical reasoning: A study
cites work: A Brief Overview of HOL4
DOI: 10.1007/S10817-010-9169-Y
description: scientific article; zbMATH DE number 5903837