BEDWYR(1) User’s Reference Manual BEDWYR(1)
bedwyr, bedwyr.byte, bedwyr.native — the not-so-sound logician
bedwyr [−I] [−t] [−T] [−−filter] [−d command] [−e query] [−−freezing fp] [−−saturation sp] [−−version] [−D] [−−colour n] [−help|−−help] [file ...]
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 ,
The wrapper bedwyr is the preferred invocation.
Do not enter interactive mode.
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 "
Run tests in all definition files.
Use tabling with variables. If not set, only strict matches are used.
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.
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.
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.
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.
Display version information and a list of compiled features.
Print debugging information on stderr. Can be enabled/disabled at run-time with #debug.
Force the number of supported colours. 256 and 8 assume the corresponding number of ANSI colours, anything else disables the coloured output.
Display the list of command-line options.
The bedwyr utility exits 0 on success, and >0 if an error occurs.
Input error (base syntax error, type error)
Command error (wrong declaration, wrong definition)
Solver error (LLambda violation, Level 0/1 violation, object misuse)
Bedwyr error (failed assertion, meta-command misuse)
A definition file can contain any meta-command (see META-COMMANDS), in addition to any of the following commands.
Kind list type −> type.
nat, string and prop are built in, while list and option are predeclared.
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.
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).
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).
Interactive toplevel. Queries can span on several lines, but all input between the . and the end of the line is ignored.
bedwyr −e "
Non-interactive toplevel. The string must not be empty, and all input between the . and the end of the line is ignored.
Meta-commands can be given both in a file and to the toplevel.
This command should give a starting point.
And this one, an ending point.
Non-interactive output is offerd by #save_table pred "
table.def ". or #export "
Sample input files. Most of them have assertions that can be checked with the command-line option −t.
Bedwyr v1.4-beta9 June 16, 2015 Bedwyr v1.4-beta9