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 (ITP04), Rennes, France. LNCS 7998, pp. 386–401. July 2013. ©Springer
0. Download
Profound is developed on GitHub. The 0.3 alpha release can be downloaded as a tar.gz or as a zip file. You can also follow the development by cloning the repository:
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:
 Batteries Included (version 2.0 or later)
 Findlib
 LablGTK2
 Menhir
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/opamkc.tar.gz && tar C ~ xf opamkc.tar.gz $ opam repo add opamkc ~/opamkc $ 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.
2. Building
There is nothing to configure.
Just run make
.
It will produce the binary ./profound.native
.
3. Invoking
Use the 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.
4.1. Navigation
Navigation in the subformula tree is done with the cursor keys (Up
,
Down
, Left
and Right
). The current selected subformula is
indicated in braces {}
.
To start navigating, you will have to descend at least once (with the
Down
key).
Hit ShiftUp
to stop navigating subformulas, i.e., to go all the way
back to the top.
4.2. Linking
The primary operation that the user is expected to perform is linking.
To initiate a link (technical term: mark a source), press the Return
or 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 ?.
Then hit Return
or 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.
4.3. History
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 CtrlZ
.
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
hitting CtrlY
.
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 histlines
command line
parameter, and dynamically using the +
and 
keys.
4.4. Saving and quitting
To quit, hit CtrlQ
.
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 CtrlS
.
4.5. Other interactions
On any subformula

Delete
rewrites it to 0. Note that0 \plus A
andA \plus 0
will be rewritten toA
eagerly when ascending out of the current context.
If the current subformula is a ?formula and has no marks in any subformula, then:

ShiftReturn
/ShiftEnter
contracts it, i.e., it rewrites ?A to ?A \par ?A. 
ShiftDelete
applies weakening to it, i.e., it rewrites ?A to \bot. 
?
applies dereliction to it, i.e. it rewrites? A
toA
.
If the current subformula is an existential, then:

ShiftReturn
opens 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 (sansserif) font.
4.6. Concrete syntax
Formulas in theorems use the following concrete syntax:
 Atomic formulas: firstorder predicates. Example:
p(f(x), g(x, y))
 Negated atoms:
\lnot
or~
. Example:~ p(f(x), g(x, y))
 Tensor:
\tensor
or*
. Examples:a \tensor b
,a * b
 One (unit of Tensor):
\one
or1
 Plus:
\plus
or+
. Examples:a \plus b
,a + b
 Zero (unit of Plus):
\zero
or0
 Par:
\par
or
. Examples:a \par b
,a  b
 Bottom (unit of Par):
\bot
or#F
 With:
\with
or&
. Examples:a \with b
,a & b
 Top (unit of With):
\top
or#T
 Bang:
!
. Example:!a
 Whynot:
?
. Example:?a
 Universal quantification:
\A
with commaseparated variables terminated by a.
. Example:\A x, y. p(x, f(y))
.  Existential quantification:
\E
with commaseparated variables terminated by a.
. Example:\E x, y. p(x, f(y))
.
Identifiers must match the regexp [AZaz][AZaz09_]*
Some example theorems can be found in the examples/
subdirectory.
5. License and copyright
Copyright (c) 2013, Inria.
See the file LICENSE (a standard 2clause BSD) for licensing details