Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm

DOI10.1007/BF00249356zbMATH Open0723.68072OpenAlexW2011482734MaRDI QIDQ757074FDOQ757074

Authors: Matt Kaufmann 

Publication date: 1991

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00249356

Recommendations

• Extensions to a generalization critic for inductive proof
• General correctness: A unification of partial and total correctness
• Higher order generalization and its application in program verification
• scientific article; zbMATH DE number 2086517
• Automated Reasoning
• On the construction of a generalized computational experiment in verification problems
• A general solution to (free) deterministic equivalents
• Generalization strategies for the verification of infinite state systems
• A generalization of context-free determinism

zbMATH Keywords

generalizationcase studyBoyer-Moore theorem proverfree variablesproof-checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (2)

• A theorem prover for a computational logic
• Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem

Uses Software

• HOL
• Nuprl
• LISP

This page was built for publication: Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm

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