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

DOI10.1007/BF00249356zbMath0723.68072OpenAlexW2011482734MaRDI QIDQ757074

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

case studygeneralizationBoyer-Moore theorem proverfree variablesproof-checking

Mathematics Subject Classification ID

Related Items (1)

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