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

DOI10.1007/BF00249356MaRDI QIDQ757074zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

generalizationcase studyBoyer-Moore theorem proverfree variablesproof-checking

Mathematics Subject Classification ID

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

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

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

Describes a project that uses

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)