HTab

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

NAME

htab − terminating tableaux system for hybrid logic

SYNOPSIS

htab [−s] [−st stats] [−t secs] [−cd directory] [−lo output.tex] [−gm model] [−sb [0|1] [-fc [0|1]] −f formula.frm

DESCRIPTION

HTab is a theorem prover and model builder for the basic hybrid logic, guaranteeing termination for all formulas.

OPTIONS

−s

display the internals of the tableaux and the rules used during the calculus

−lo output.tex

create a LaTeX file of the internals of the tableaux and the rules used during the calculus

−cd

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

−sb [0|1]

enable/disable semantic branching (default is enabled)

−fc [0|1]

enable/disable full clash (default is enabled)

−t

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

−gm model.out

generate a model for the input formula, into the file model.out

−st pattern

print statistics during of after the execution. A valide pattern is of the form:

METRICS:INTERVAL:METRICS

The ‘:INTERVAL:METRICS‘ argument is optional and declares metrics that will be printed at regular intervals (e.g. ‘:100:r’ shows the number of rules applied so far, every 100 iterations of the algorithm).
METRICS is made of one or more of the following values:

c : number of closed branches

r : number of rules applied

The default is ’:0:c’

FILES

~/.htabrc configuration file

EXAMPLES

Run HTab without semantic branching nor full clash, and write the tableaux states into out.tex:

htab −sb 0 −fc 0 −lo out.tex −f formula.frm

Run HTab by reading the .htabrc file of the current directory:

htab −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 |
’(’ 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

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

.htabrc SYNTAX

See the comments in the .htabrc file generated by HTab.

AUTHOR

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

AVAILABILITY

Home page

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

Code repository

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