GOAL: A Goal Oriented Command Language for Interactive Proof Construction
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
This thesis represents a contribution to the development of practical computer systems for interactive construction of formal proofs. Beginning with a summary of current research in automatic theorem proving, goal oriented systems, proof checking, and program verification, this work aims at bridging the gap between proof checking and theorem proving. Specifically, it describes a system GOAL for the First Order Logic proof checker FOL. GOAL helps the user of FOL in the creation of long proofs in three ways 1 as a facility for structured, top down proof construction 2 as a semi-automatic theorem prover and 3 as an extensible environment for the programming of theorem proving heuristics. In GOAL, the user defines top level goals. These are then recursively decomposed into subgoals. The main part of a goal is a well formed formula that one desires to prove, but they include assertions, simplification sets, and other Information. Goals can be tried by three different types of elements matchers, tactics, and strategies. The matchers attempt to prove a goal directly -that is without reducing it into subgoals- by calling decision procedures of FOL. Successful application of a matcher causes the proved goal to be added to the FOL proof. A tactic reduces a goal into one or more subgoals. The strategies are programmed sequences of applications of tactics and matchers.
- Computer Programming and Software
- Computer Hardware