Profound is an experiment in subformula linking as an interaction method. Its theoretical basis is found in this document:
- K. Chaudhuri. Subformula Linking as an Interaction Method. Conference on Interactive Theorem Proving (ITP-04), Rennes, France. LNCS 7998, pp. 386–401. July 2013. ©Springer
git clone https://github.com/chaudhuri/profound.git
Please note that this is alpha quality software that is under active development.
1. Building Prerequisites
You will need OCaml (version 3.12.1 or later) and the following packages:
Consider using OPAM and a recent version (4.00.0+) of OCaml and the most recent versions of the above libraries. Until I add Profound to the main OPAM repository, you can get it with a local OPAM repository as follows (not recomended for novices).
$ wget http://kaustuv.chaudhuri.info/uncat/opam-kc.tar.gz && tar -C ~ -xf opam-kc.tar.gz $ opam repo add opam-kc ~/opam-kc $ opam install profound
This command will install all the dependencies for you.
You will also need a LaTeX distribution (eg. TeXLive) that contains AMS Math and dvipng.
It will probably only work on a Linux system.
There is nothing to configure.
It will produce the binary
--help option for a quick overview of all options.
Theorem in the command line
$ ./profound.native "a | ~a"
Theorem read from a file
$ echo "a | ~a" > a.p $ ./profound.native -i a.p
4. User Interface
Profound has a very minimalistic user interface.
The main theorem is displayed centered in the window.
The only other widget is a small status bar that sometimes displays hints or error messages.
Navigation in the subformula tree is done with the cursor keys (
Right). The current selected subformula is
indicated in braces
To start navigating, you will have to descend at least once (with the
Shift-Up to stop navigating subformulas, i.e., to go all the way
back to the top.
The primary operation that the user is expected to perform is linking.
To initiate a link (technical term: mark a source), press the
Enter keys. This will turn the current selection blue. Any
subformula of the theorem can be a source – not just the atoms.
To complete a link (technical term: mark a sink), navigate to another
subformula that is ancestrally joined to the source via a par or a ?.
Enter again. Any suitable subformula can be a
sink, not just atoms.
When a link completes, the source and sink interact hereditarily, with all ties broken in favor of the sink having outermost scope. Intuitively, the source is “brought to” the sink.
The proof state is presented as a linear timeline with the present shown in the middle in a large font, and the past and future below and above the present.
Whenever a link is resolved or the current theorem is rewritten, the previous state of the theorem is prepended to the past.
To go back to an earlier form, hit
Going back in history shows the known future above the theorem line.
You can return to any of the futures in the current timeline by
Note that any rule application that modifies the text of the theorem will alter the current timeline and therefore will remove the futures from the earlier timeline. (There is currently no way to restore a lost timeline – after a number of experiments, I came to the conclusion that allowing too much branching in time adds only confusion.)
By default only the three most recent past and future states are
shown. You can change this with the
-hist-lines command line
parameter, and dynamically using the
4.4. Saving and quitting
To quit, hit
If the input came from a file, the current state of the proof is saved on quitting. When working on the same file again, the previous state is restored, including the full undo and redo histories.
A save can also be forced at any time using
4.5. Other interactions
On any subformula
Deleterewrites it to 0. Note that
0 \plus Aand
A \plus 0will be rewritten to
Aeagerly when ascending out of the current context.
If the current subformula is a ?-formula and has no marks in any subformula, then:
Shift-Entercontracts it, i.e., it rewrites ?A to ?A \par ?A.
Shift-Deleteapplies weakening to it, i.e., it rewrites ?A to \bot.
?applies dereliction to it, i.e. it rewrites
If the current subformula is an existential, then:
Shift-Returnopens a dialog box asking for a witness to substitute for the variable. Witnesses are allowed to use any of the variables in scope of the existential – these will be captured. All free identifiers in the witness terms are assumed to be signature constants, and are displayed in a different (sans-serif) font.
4.6. Concrete syntax
Formulas in theorems use the following concrete syntax:
- Atomic formulas: first-order predicates. Example:
p(f(x), g(x, y))
- Negated atoms:
~ p(f(x), g(x, y))
a \tensor b,
a * b
- One (unit of Tensor):
a \plus b,
a + b
- Zero (unit of Plus):
a \par b,
a | b
- Bottom (unit of Par):
a \with b,
a & b
- Top (unit of With):
- Universal quantification:
\Awith comma-separated variables terminated by a
\A x, y. p(x, f(y)).
- Existential quantification:
\Ewith comma-separated variables terminated by a
\E x, y. p(x, f(y)).
Identifiers must match the regexp
Some example theorems can be found in the