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 "

file.def "..


Run tests in all definition files.


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.


Display version information and a list of compiled features.


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.


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)


Undefined error


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.


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).

?= query.

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.


Text-mode goodies.



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