HyLoBan

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
FILES
EXAMPLES
INPUT FILE SYNTAX
.hylobanrc SYNTAX
AUTHOR
AVAILABILITY

NAME

HyLoBan − game-based terminating system for hybrid logic with topological semantics

SYNOPSIS

hyloban [−s] [−t secs] [−cd directory][−t0] [−t1] [-c] −f formula.frm

DESCRIPTION

HyLoBan is a theorem prover for hybrid logic equipped with the universal modality, on topological semantics with separation axioms T0 and T1, guaranteeing termination for all formulas of the input language.

OPTIONS

−s

display the internals during the calculus

−cd

specify a directory where the configuration file (.hylobanrc) should be read and written (default is $HOME)

−c

enable caching (default is disabled)

−t

set the timeout (in seconds). Default is no timeout.

−t0

enable topological axiom T0 (default)

−t1

enable topological axiom T1

FILES

~/.hylobanrc configuration file

EXAMPLES

Run HyLoBan with caching, and display the internal states:

hyloban −c −s −f formula.frm

Run HyLoBan by reading the .hylobanrc file of the current directory:

hyloban −cd . −f formula.frm

INPUT FILE SYNTAX

The grammar for the files accepted by the prover is specified below. Comments of the form ’{’ ALPHANUMERIC ’}’ are accepted anywhere in the file.

FILE := ’begin’ FORMULAS ’end’
FORMULAS := FORMULA | FORMULA ’;’ FORMULAS
FORMULA :=
’true’ | ’false’ |
PROPOSITION | NOMINAL |
NEGATION | CONJUNCTION | DISJUNCTION | IMPLICATION | DIMPLICATION |
BOX | DIAMOND | AT | EXISTS |
’(’ FORMULA ’)’
PROPOSITION := ’P’ NUMBER | ’p’ NUMBER
NOMINAL := ’N’ NUMBER | ’n’ NUMBER
RELATION := ’R’ NUMBER | ’r’ NUMBER
NEGATION := ’!’ FORMULA | ’-’ FORMULA | ’~’ FORMULA
CONJUNCTION := FORMULA ’&’ FORMULA | FORMULA ’^’ FORMULA
DISJUNCTION := FORMULA ’|’ FORMULA | FORMULA ’v’ FORMULA
IMPLICATION := FORMULA ’->’ FORMULA
DIMPLICATION := FORMULA ’<->’ FORMULA
BOX := ’[]’ FORMULA | ’box’ FORMULA | ’[’ RELATION ’]’ FORMULA
DIAMOND := ’<>’ FORMULA | ’dia’ FORMULA | ’<’ RELATION ’>’ FORMULA
AT := NOMINAL ’:’ FORMULA | ’@’ NOMINAL FORMULA
EXISTS := ’E’ FORMULA

See also the example formulas in /usr/share/doc/hyloban/examples or /usr/local/share/doc/hyloban/examples

.hylobanrc SYNTAX

See the comments in the .hylobanrc file generated by HyLoBan.

AUTHOR

Guillaume Hoffmann (guillaume.hoffmann (at) loria.fr)

AVAILABILITY

Home page

http://hylo.loria.fr/intohylo/hyloban.php

Code repository

http://trac.loria.fr/projects/hyloban