Title :
A survey of mechanical support for formal reasoning
Author :
Lindsay, Peter A.
Author_Institution :
Manchester Univ., UK
fDate :
1/1/1988 12:00:00 AM
Abstract :
The article is a survey of computer support for formal reasoning, but primarily from the point of view of software engineering applications. It is an introduction to existing systems and ongoing research, gathering together information which has often only appeared before in narrowly distributed technical reports. Formal reasoning means the deduction of logical expressions from other logical expressions. Usually the expressions represent properties of (and relationships between) mathematical entities
Keywords :
program verification; software engineering; specification languages; theorem proving; Affirm; Boyer-Moore prover; Gypsy environment; Isabelle; LCF; NuPRL; Veritas; computer support; existing systems; formal reasoning; logical expressions; mathematical entities; ongoing research; software engineering;
Journal_Title :
Software Engineering Journal
