1 Introduction
The package fricas_snark is an interface to SNARK, SRI’s New Automated
Reasoning Kit, a theorem prover intended for
applications in artificial intelligence and software engineering. SNARK is
geared toward dealing with large sets of assertions; it can be specialized
with strategic controls that tune its performance; and it has facilities
for integrating special-purpose reasoning procedures with general-purpose
inference.
The goal is to have a powerful automated theorem prover (ATP in the sequel)
combined with the algebraic power of FriCAS. Since SNARK is being developed
in Common Lisp (on which FriCAS is mainly built on), it is not difficult to
interface the prover on the Lisp level (see src/snark.lisp). A new domain
called Propositions (abbrev. PROP) builds the link between FriCAS’
algebraic language (SPAD) and SNARK’s own logic language in CL which is close
to the [KIF] standard (actually KIF is an option).
The end user will be able to use most of SNARK’s features on the SPAD level,
however, it is always possible, of course, to access the CL level by using
FriCAS’ Lisp interface - )lisp or )fin. So this documentation will
focus on the Proposition domain, whereas for the Common Lisp part (CL in
the following) we refer to the SNARK documentation [tutorial], [paper],
[home], [author]. For the understanding of the ATP it is certainly necessary
to be acquainted with the SNARK tutorial.