BEDWYR(1) User’s Reference Manual BEDWYR(1)

NAME

bedwyr, bedwyr.byte, bedwyr.native — the not-so-sound logician

SYNOPSIS

bedwyr [−I] [−t] [−T] [−−filter] [−d command] [−e query] [−−freezing fp] [−−saturation sp] [−−version] [−D] [−−colour n] [−help|−−help] [file ...]

DESCRIPTION

Bedwyr is a tabled logic programming system for the Level-0/1 fragment of the Linc logic.

It is based on Tiu’s Level-0/1, and Nadathur & Linell’s LLambda library. For background on the system, see

Alwen Tiu ,
Gopalan Nadathur , and
Dale Miller ,
Mixing Finite Success and Finite Failure in an Automated Prover
,
http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/eshol05.pdf .

Webpage: http://slimmer.gforge.inria.fr/bedwyr/.

The wrapper bedwyr is the preferred invocation.

OPTIONS
−I

Do not enter interactive mode.

−t

Run tests (given by #assert query., see META-COMMANDS) from the definition files given on the command-line. Use n+1 times to test also files that occured under up to n levels of #include "

file.def "..

−T

Run tests in all definition files.

−−filter

Use tabling with variables. If not set, only strict matches are used.

−d command

Run command (declaration of definition, see INPUT FILES). Multiple commands can be given. They are run after all the input files are read, and before executing queries.

−e query

Execute query (see TOPLEVEL QUERIES). Multiple queries can be given. They are executed after all the commands are run, and before entering the interactive loop.

−−freezing fp

Enable backward chaining and set its limit (the so-called freezing-point) to fp. Setting it to 0 (the default value) disables backward chaining, setting it to −1 allows for infinite chaining (usually not a smart idea). The value 1 should be a good compromise.

−−saturation sp

Enable forward chaining and set its limit (the so-called saturation-point) to sp. Setting it to 0 (the default value) disables forward chaining, setting it to −1 allows infinite chaining and therefore actual saturation of the table wrt the theorem.

−−version

Display version information and a list of compiled features.

−D

Print debugging information on stderr. Can be enabled/disabled at run-time with #debug.

−−colours n

Force the number of supported colours. 256 and 8 assume the corresponding number of ANSI colours, anything else disables the coloured output.

−help, −−help

Display the list of command-line options.

EXIT STATUS

The bedwyr utility exits 0 on success, and >0 if an error occurs.

1

Input error (base syntax error, type error)

2

Command error (wrong declaration, wrong definition)

3

Solver error (LLambda violation, Level 0/1 violation, object misuse)

4

Bedwyr error (failed assertion, meta-command misuse)

5

Undefined error

INPUT FILES

A definition file can contain any meta-command (see META-COMMANDS), in addition to any of the following commands.

Type declaration

Kind list type −> type.

nat, string and prop are built in, while list and option are predeclared.

Constant declaration

Type :: A −> list A −> list A.

Type nil list A.

true and false are built-ins of type prop, 0, 1, ... and any quoted string are runtime-defined constants of type nat and string, and ::, nil, some and none are predeclared.

Predicate declaration and definition

Define member : A −> list A −> prop by member X (X :: _) ; member X (_ :: L) := member X L.

print, println, printstr, fprint, fprintln, fprintstr, fopen_out and fclose_out are built in, member is predefined.

Theorems

Theorem thm : forall Y, body X Y −> head X.

A theorem is a valid Abella theorem with some restrictions on its body (neither implication nor universal quantification).

TOPLEVEL QUERIES

The toplevel input can contain any meta-command (see META-COMMANDS), as well as any formula. In the latter case, each formula is a query which is solved (bedwyr searches for all substitutions of free variables satisfying query and offers to display them one by one).

?= query.

Interactive toplevel. Queries can span on several lines, but all input between the . and the end of the line is ignored.

bedwyr −e "
query
."

Non-interactive toplevel. The string must not be empty, and all input between the . and the end of the line is ignored.

META-COMMANDS

Meta-commands can be given both in a file and to the toplevel.

#help.

This command should give a starting point.

#exit.

And this one, an ending point.

OUTPUT

Non-interactive output is offerd by #save_table pred "

table.def ". or #export "
tables.xml
"..

FILES
/usr/local/share/bedwyr/examples/

Sample input files. Most of them have assertions that can be checked with the command-line option −t.

/usr/local/share/bedwyr/contrib/

Text-mode goodies.

SEE ALSO

teyjus(1)

Bedwyr v1.4-beta9 June 16, 2015 Bedwyr v1.4-beta9