Psyche is a modular platform for
automated or interactive theorem proving, programmed in OCaml and built on an architecture
(similar to LCF) where a small kernel interacts with plugins and decision procedures:
- The kernel offers an API to perform proof-search in various inference systems that can be combined.
- Plugins can be programmed to drive the kernel, using its API, through the search space towards
an answer
*provable* or *not provable*; soundness of the answer only relies on the kernel via the
use of a private type for answers (similar to LCF’s *theorem* type).
- Psyche's inference systems form the basis of two main components: Psyche' front-end and Psyche's back-end.
- The front-end implements a proof-search engine
*à la* Prolog, performing incremental
and goal-directed constructions of proof-trees in (a standard but carefully chosen) Sequent
Calculus, which can be seen as a tableau method.
- The back-end is used when the front-end seeks to close a branch, and different back-ends can be used.
- One of them is a first-order unification procedure, which allows Psyche to tackle pure first-order logic problems
- The other one is a ground theory combinator module, which allows Psyche to tackle (quantifier-free) SMT problems;
it takes a list of theory modules, and provides a module for their union.
The ultimate goal is to have the two modes collaborate.
- Plugins can be interactive, which is most useful for the plugin driving the front-end engine,
while plugins for the back-end modules are (but don't have to be) automated.
- Psyche can produce proof objects.
- Psyche offers a memoisation feature to help programming efficient plugins.
The current version 2.1 of Psyche is distributed
- with a front-end plugin driving the sequent calculus proof-search engine;
on quantifier-free problems, the plugin makes the front-end emulate DPLL(T),
using watched literals to propagate literals or close
branches, and Psyche’s memoisation feature to learn lemmas;
- with a first-order unification back-end for pure first-order logic problems;
- with decision procedures that can be passed to the ground theory combinator back-end:
boolean logic and Congruence Closure, and a beta version of Linear Rational Arithmetic (LRA);
- with an SMTLib2 parser and a DIMACS parser;
- as a program of about 10 000 lines of OCaml 4.
Psyche does not claim to be a better SAT- or SMT-solver or first-order theorem prover than any existing
one: the heuristics for applying DPLL(T) rules in the aforementioned plugin are for instance still basic, and so
is the decision procedure for LRA (it is not incremental). What we offer here is a platform and its
modularity: anyone with better (or different) heuristics and decision procedures can simply write
them as OCaml modules of our predefined module types, and Psyche will seamlessly run with
them, keeping the same LCF-style guarantees.
More motivation about the architecture can be found in the documents.
Psyche is developped at the Laboratoire d'Informatique de l'X (and it was initiated by the PSI project). Direct contributors include Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin,
Alexis Bernadet,
Mahfuza Farooque,
Guillaume Hétier,
Zelda Mariet,
Clément Pit-Claudel,
Damien Rouhling,
André Schrottenloher,
Matthieu Vegreville. |