LinearOne
This research has received financial support from the ANR CONTINT, project POLYMNIE (ANR-12-CORD-0004).
LinearOne is a prototype theorem prover/parser for first-order (multiplicative, intuitionistic) linear logic. It also supports (by translation) parsing of hybrid type-logical grammars and Displacement calculus grammars.
LinearOne is provided under the GNU Lesser General Public License (see the included file LICENSE for details).
LinearOne is a set of SWI Prolog files, which optional graph output to LuaLaTeX (using the TikZ 3.0.0 graph drawing libraries) and proof output to LaTeX/pdfLaTeX/luaLaTeX.
Quick start
Starting Prolog
After downloading, enter the LinearOne directory and type.
swipl # (or the name of SWI Prolog on your system)
This will start SWI Prolog.
Loading the source and the grammars
In SWI Prolog, type
[mill1,d_grammar].
to load the library files and the example Displacement calculus grammar, there is a hybrid type-logical grammar available as well.
[hybrid_grammar].
Parsing
To try one of the examples in either grammar, use
test(1). % (check the grammar files to see the available examples).
You can also use
parse([john,ate,more,donuts,than,mary,bought,bagels], s).
to directly parse a sentence. Check the lexicon and experiment a bit with the grammars yourself.
Viewing the output
When a parse is found, it is output to the file latex_proofs.tex and a pdf file latex_proofs.pdf is automatically produced. View latex_proofs.pdf with your favorite previewer. You will probably need to zoom in for larger proofs.
Troubleshooting
No LaTeX output is produced!
Make sure that you have write permissions in the LinearOne directory and that Prolog can find your LaTeX installation. To find the location of pdflatex type the following in a shell terminal
where pdflatex
Add the required path to the file mill1.pl. For example, the path /usr/texbin/ is added as follows.
user:file_search_path(path, '/usr/texbin/').
It is also possible that LaTeX aborts with an error (verify the file latex_proofs.tex).
The proofs don't fit the page!
The geometry/1 predicate in the file latex.pl can be modified to the desired page size. Comment out all but the desired page size (or add your own preferred page size). Zooming will be necessary!
I don't see any graph output
Graph output is optional. In the file mill1.pl, comment out the line
use_module(portray_graph_none,...)
and remove the comments from line
use_module(portray_graph_tikz,...)
Also make sure your LaTeX installation includes lualatex and Tikz 3.0.0 or later (that is, you need a 2014 or later LaTeX installation).