richardmoot / linearone Goto Github PK

LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.

License: GNU Lesser General Public License v2.1

Makefile 0.01% Prolog 99.99%

linear-logic first-order-logic theorem-proving proof-net displacement-calculus-grammars swi-prolog logic-programming latex

linearone's Introduction

LinearOne

©️ 2015-2019 CNRS

©️ 2015-2019 Richard Moot (@RichardMoot)

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).

linearone's People

Contributors

Stargazers

Watchers

Forkers

symonjorystevens-guille verceti-ke

linearone's Issues

Add/evaluate a choice of tie-breakers to the dancing links algorithm

LinearOne fails to find some proofs

Allow complex terms

The beta version allows a predicate to have only variable or constant terms. Some of the more subtle applications of first-order linear logic require complex terms. For example, the treatment of associativity and scope restrictions in my 2014 Lambek paper uses "integer-like" terms (of the forms s(X), s(s(X), etc.)

Produce eta-normal proofs

Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to produce eta-normal proofs as well.

Add an (optional) proof transformation step which transforms long normal form proofs into beta-eta-normal proofs.

Dancing links

Implement smarter axiom link strategy, selecting the axiom which has the least possible partner (similar to the Grail 3 strategy and to Knuth's general Dancing Links algorithm).

Extend proof generation

Implement cut elimination

Variable names

The variable renaming can produce inconsistent results in complex cases. This needs to be corrected.

Add examples

Add many more examples from the papers of Morrill e.a. and Kubota & Levine as additional test cases.

Add support for features

One of the most basic applications of first-order linear logic is its application for linguistic features such as Case, Gender, Number etc. Though this is easily implemented in first-order linear logic itself, it would be useful to add the possibility of incorporating features into the translation functions for the Displacement calculus and hybrid type-logical grammars

Add support for additives

Add additives together with a contraction condition as proposed by Maieli.

This will be a major update/rewrite since it will complicate (at least) the axiom linking component: it will allow an atom to not be linked at all (if a plus link "erases" it) or to be linked multiple times (if it has a contraction link as a parent).

Translate proofs into Displacement calculus

Add translation of first-order linear logic proof (natural deduction and/or sequent calculus) into Displacement calculus proofs.

Translate proofs into Lambek calculus, Displacement calculus, hybrid or lambda grammar proofs.

Add position constraints

Allow specification of constraints of the form X=<Y. These constraints will help with the treatment the reflexives of the Displacement calculus, but they are a simple and powerful mechanism in general.

The constraint-like implementation will essentially be the following
X =< X <=> true
X =< Y, integer(X), integer(Y) <=> Prolog's X =< Y for integers (evaluates to true or false)
X =< Y, Y =<X <=> X = Y
X =< Y, Y =< Z => X =< Z (only rule which adds constraint)

Better constraints for forall links

Forall links have the property that no atom containing the eigenvariable of a link can every be identified with a node which dominates the forall link of this variable. Adding this constraint would reduce the search space and make testing the forall contraction less complicated.