Some law applications may require the satisfaction of certains condition under which the law
application is valid. The proof obligations generated during the development are shown in
the Proof Obligations window.
After being generated, the proof obilgations are given to the theorem prover that tries to verify the validity of the condition. Currently, this theorem prover is internal to CRefine and small; it verifies only some of the syntactic restrictions. For this reason, a status is given to each proof obligation. This status can be:
(true),
(false),
(undetermined),
(manually proven true) and 
(manually proven false).
by selecting the proof obligation, the line in the development window that corresponds to the law application that generated the proof obligation is highlighted.
An important functionality, offered by CRefine's current theorem proving facilities, is to give to the user the choice of seeing the proof obligations in its expanded format using the definitions of the syntactic functions. In order to see the expanded or contracted version of the proof obligations, the user must select the proof obligation and click on the right button of the mouse: a pop-up menu is shown to the user. Using this pop-up menu, we have access to three important functionalities: manual proof, edit, and show.
The manual proof allows the user to define the proof obligation status for those proof obligations that could not be proved by CRefine theorem proving facilities. As the name suggests, these proofs must have been manually done by the user. After setting the status of a proof obligation, the proof obligation window is updated accordingly. The action of setting a status for proof obligations can also be undone/redone.
Another functionality is the exhibition of proof obligations in either expanded or contracted format. The latter is the standard format. The former applies the definitions of the syntactic functions to show the calculated predicates. For this reason, only those proof obligations with syntactic functions on it can be exanded/contracted. In order to select the format, start the pop-up menu of the proof obligation window and select "Show -> Expanded". Analogously, we have the "Show -> Contracted" option.
After choosing the new format the proof obligation is shown in the desired format. This action can also be undone/redone.
The functionality of copying the text of a proof obligation to the system clipboard is describe in Copy.
After being generated, the proof obilgations are given to the theorem prover that tries to verify the validity of the condition. Currently, this theorem prover is internal to CRefine and small; it verifies only some of the syntactic restrictions. For this reason, a status is given to each proof obligation. This status can be:
(true),
(false),
(undetermined),
(manually proven true) and (manually proven false).
by selecting the proof obligation, the line in the development window that corresponds to the law application that generated the proof obligation is highlighted.
An important functionality, offered by CRefine's current theorem proving facilities, is to give to the user the choice of seeing the proof obligations in its expanded format using the definitions of the syntactic functions. In order to see the expanded or contracted version of the proof obligations, the user must select the proof obligation and click on the right button of the mouse: a pop-up menu is shown to the user. Using this pop-up menu, we have access to three important functionalities: manual proof, edit, and show.
The manual proof allows the user to define the proof obligation status for those proof obligations that could not be proved by CRefine theorem proving facilities. As the name suggests, these proofs must have been manually done by the user. After setting the status of a proof obligation, the proof obligation window is updated accordingly. The action of setting a status for proof obligations can also be undone/redone.
Another functionality is the exhibition of proof obligations in either expanded or contracted format. The latter is the standard format. The former applies the definitions of the syntactic functions to show the calculated predicates. For this reason, only those proof obligations with syntactic functions on it can be exanded/contracted. In order to select the format, start the pop-up menu of the proof obligation window and select "Show -> Expanded". Analogously, we have the "Show -> Contracted" option.
After choosing the new format the proof obligation is shown in the desired format. This action can also be undone/redone.
The functionality of copying the text of a proof obligation to the system clipboard is describe in Copy.