## A Quick-Start Guide to |

Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expression.

The logic manipulated, a subset of LINC (for *lambda, induction,
nabla, co-induction*), contains object-level λ-abstractions,
∇ (nominal) quantification, and (co-)inductive definitions.
While LINC is a extension of higher-order intuitionistic logic, Bedwyr
formulae are restricted to a fragment where connectives on the left of
an implication must have invertible rules (i.e. no universal
quantifier nor implication – this enables the closed-world assumption
when identifying finite success and finite failure), while equalities
are restricted to the L_{λ} fragment (allowing for the use of
higher-order pattern unification).

The OCaml implementation is part of an open source project. The web page offers multiple ways to get it:

- SVN repository
- tarballs
- precompiled binaries
- GNU/Linux packages
- Windows installer

The documentation includes this quick-start guide, a reference manual and the source-code documentation.

Input sources can be plain text definition files (*.def), the
REPL (read-eval-print loop), the
`read`

predicate, and
arguments to the -d, -e and -c CLI
(command-line interface) options. Three modes are available:

- definition mode
- is used in *.def files and with -d
- toplevel mode
- is used in the REPL and with -e
- term mode
- is used at run-time via
`read`

and with -c

Commands are used in definition mode to declare new types and constants, declare and define predicates, and define theorems (which are not proved, but are used as lemmas).

Queries are plain formulae (terms of type
`prop`

), entered
at the toplevel, that Bedwyr attempts to solve. If possible, it
outputs the list of solutions (substitutions of the free variables).
Otherwise, if the formula is not handled by the prover (non-invertible
connective on the left) or by the unifier (not L_{λ}), resolution
aborts.

Meta-commands are used both in definition mode and at the toplevel,
mostly to improve the user experience by executing strictly
non-logical tasks, such as input (
`#include "inc.def".`

),
output (
`#typeof X Y :: nil.`

) or testing
(
`#assert true.`

). A few of them change proof structure,
but not provability (
`#freezing 4.`

,
`#saturation 2.`

).

Term-mode is a way to improve interactivity.

1 shows a complete sample definition file, with the declarations for a type and two constants, along with a few predicates.

Kindch type.Typez ch.Types ch -> ch. % The predicate a holds for 3, 5, and 2.Definea : ch -> propbya (s (s (s z))) ; a (s (s (s (s (s z))))) ; a (s (s z)). % The less-than-or-equal relationDefineinductiveleq : ch -> ch -> propbyleq z _ ; leq (s N) (s M) := leq N M. % Compute the maximum of aDefinemaxa : ch -> propbymaxa N := a N /\ forall x, a x -> leq x N.

The predicate
`a`

is a typical example of what must be done to build
a Bedwyr example: even with a theoretically infinite search space
(here, Church numerals), Bedwyr only does finite reasoning, and hence must be
given an explicit description of its finite actual search space.

The use of the

keyword has two consequences.
Firstly, memoization is used on the corresponding predicate;
secondly, it has an impact on the way loops in computation are handled.
Since the
__inductive__`leq`

predicate obviously cannot loop,
only the first aspect is used here (meaning we might as well have used the

keyword instead).__coinductive__

2 shows an example of use of the interactive toplevel
following the invocation of `bedwyr maxa.def`

.

?= #env. *** Types *** option : * -> * list : * -> * ch : * *** Constants *** (::) : A -> list A -> list A nil : list A opnone : option A opsome : A -> option A s : ch -> ch z : ch *** Predicates *** a : ch -> prop I leq : ch -> ch -> prop maxa : ch -> prop member : A -> list A -> prop ?= read Y /\ leq X Y. ?> s z. Solution found: X = z Y = s z More [y] ? y Solution found: X = s z Y = s z More [y] ? y No more solutions. ?= maxa X. Solution found: X = s (s (s (s (s z)))) More [y] ? y No more solutions. ?= #exit.

The
`#env.`

meta-command shows all declared objects
(including the standard pre-declared list-related objects), and
informs
`leq`

is inductive. The call to the queries
`leq X (s z).`

and
`maxa X.`

offer to display all
solutions, one by one.
A subsequent call to
`#show_table leq.`

would show the table
filled by the second query with
`leq`

-headed atoms, either
marked as proved or disproved.

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.