robsimmons

- val {get, poll} = Conductor.package "/tmp/smackage" "rob-toy";
val get = fn : SemVer.semver -> unit
val poll = fn : unit -> (string * SemVer.semver) list
- poll ();
val it =
  [("02d584bf0b14704e98efc324efe6d05fb31ce4af",(0,0,1,NONE)),
   ("23597de0addda54e21d89b70f6c70ae2da75d7b8",(0,1,0,NONE)),
   ("139359d7589ca69aebfada148d8d4ad191bdeb74",(1,0,0,NONE)),
   ("0669dd7562bad0f580a0016d7b5ac88af9182512",(1,1,0,NONE)),
   ("bea772c3886a881a7a02023c89e05881a7a7ce3f",(1,1,1,NONE)),

robsimmons

/* 
   Some simple Github-like styles, with syntax highlighting CSS via Pygments.
*/
body{
	font-family: helvetica, arial, freesans, clean, sans-serif;
	color: #333;
	background-color: #fff;
	border: none;
	line-height: 1.5;
	margin: 2em 3em;

robsimmons

/* 
   Some simple Github-like styles, with syntax highlighting CSS via Pygments.
*/
body{
	font-family: helvetica, arial, freesans, clean, sans-serif;
	color: #333;
	background-color: #fff;
	border: none;
	line-height: 1.5;
	margin: 2em 3em;

robsimmons

I think some of the commenters were confused by the notation $\Gamma \vdash A \downarrow B$, which I have only seen written as $\Gamma [ A ] \vdash B$ or $\Gamma \vdash A > B$. The downarrow comes, as you note in a comment, from Andreoli's notation, but that notation is more common in presentations of sequent calculi for classical logics, at least in my experience. The notation I'll use is the one with $>$ instead of $\downarrow$, which comes from Cervesato and Pfenning's "A Linear Spine Calculus."

Two proof systems
-----------------

So, to restate the goal, we have the following sequent calculus for first-order, minimal logic:

$$
{P \in \Gamma \over \Gamma \Rightarrow P}{\it init}
\qquad

robsimmons

structure Edge:> sig

   (* Asserts some number of less-than relationships between identifiers *)
   val addRelationships: (string * string) list -> unit

   (* Returns true if two identifiers are related *)
   val related: string * string -> bool

end = struct
   open Symbol