This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** An attempt to formalize graphs. *) | |
Require Import Arith. | |
(** In order to avoid the intricacies of constructive mathematics, | |
we consider finite simple graphs whose sets of vertices are | |
natural numbers 0, 1, , ..., n-1 and the edges form a decidable | |
relation. *) | |
(** We shall work a lot with statements of the form |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
:- object(game). | |
:- info([ | |
version is 1.0, | |
author is 'Victor Lagerkvist', | |
date is 2011/03/09, | |
comment is 'The core functionality of Bacchus-Bosch.']). | |
:- public(init/0). |