gilith / metis Goto Github PK

View Code? Open in Web Editor NEW

28.0 1.0 1.0 624 KB

An automatic theorem prover for first order logic with equality

Home Page: http://www.gilith.com/metis/

License: MIT License

Makefile 2.78% Perl 3.89% Standard ML 92.33% Shell 1.00%

theorem-prover first-order-logic sml

metis's Introduction

Metis Theorem Prover (Development Version)

Metis is an automatic theorem prover for first order logic with equality. It accepts problems in TPTP format.

Cloning this repo will install a development version, which includes active debugging code and regression scripts. The latest official release of Metis without any extra development cruft lives here.

This software is released under the MIT License.

Install

Installing Metis requires the MLton, Poly/ML or Moscow ML compiler, as well as standard system tools including GNU Make and Perl.

Clone this repo and initialize the development version:

git clone https://github.com/gilith/metis.git
cd metis
make init

By default the initialization step requires the MLton compiler, but you can change it to Poly/ML or Moscow ML by editing the top of Makefile.dev.

Build

Using the MLton compiler

Use the MLton compiler to build from source and run the test suite by executing

make mlton

The Metis executable can then be found at

bin/mlton/metis

Using the Poly/ML compiler

Use the Poly/ML compiler to build from source and run the test suite by executing

make polyml

The Metis executable can then be found at

bin/polyml/metis

Using the Moscow ML compiler

Use the Moscow ML compiler to build from source and run the test suite by executing

make mosml

The Metis executable can then be found at

bin/mosml/metis

Test

A simple test is to display a usage message:

path/to/metis --help

A more serious test is to check the status of a benchmark set of problems using the command

make status-test

Troubleshoot

You can use

make clean

to clean out any object files.

To report a bug or request an enhancement, please file an issue at GitHub.

metis's People

Contributors

Stargazers

Watchers

Forkers

dataronio

metis's Issues

Simplify outputs $false, maybe wrongly.

With the following problem:

$ cat problem.tptp
fof(goal, conjecture, (((p <=> q) <=> r) <=> (p <=> (q <=> r)))).

I am getting this with Metis

$ metis --version
metis 2.3.1 (release 20161108)
$ metis --show proof problem.tptp
...
fof(normalize_2_0, plain, (~ p & (~ q <=> ~ r) & (~ p <=> (~ q <=> ~ r))),
    inference(canonicalize, [], [negate_2_0])).

fof(normalize_2_1, plain, (~ p <=> (~ q <=> ~ r)),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_2, plain, (~ q <=> ~ r),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_3, plain, (~ p), inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_4, plain, ($false),
    inference(simplify, [],
              [normalize_2_1, normalize_2_2, normalize_2_3])).
...

I do not know how simplify deduces $false in this case, maybe I am forgetting something.
Anyway, I am taking this chance to ask you about this inference? how it works.

Thanks in advance.

CC` @asr

Splitting a goal that look like ~(p <=> q)

Consider this TPTP problem

$ cat issue.tptp 
fof(goal, conjecture, (~ (p <=> q)) <=> ((p => ~ q) & (q => ~p))).

Metis finds a proof when EProver and Vampire don't. (The problem is not a tautology).

$ metis issue.tptp 
SZS status Theorem for issue.tptp

Testing with EProver with a client for SystemOnTPTP (online-atps).

$ online-atps --atp=e issue.tptp                
...
# No proof found!
# SZS status CounterSatisfiable
...

and using Vampire:

$ online-atps --atp=vampire issue.tptp  
...
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.2 (commit c955596 on 2017-07-21 22:07:53 +0100)
...
% SZS status CounterSatisfiable for SOT_wXKR
...

Metis uses this formula (above) to split goal as I found in the source of the split method, and confirmed in the test SPLIT_NOT_IFF.

So, consider this sligthly modification:

$ cat issue.tptp 
fof(goal, conjecture, (~ (p <=> q)) => ((p => ~ q) & (q => ~p))).
$ online-atps --atp=vampire issue.tptp --only-check
Theorem

I hope it be easy to fix.

Thanks in advance,

CC'ing @asr

BUG found in metis program

When launching metis with the following problem made of just one line:

fof(1,conjecture,(((Y=Z=>((X=Y=>p(X,Y,Z))&?[X]:(X=Y&p(X,Y,Z))))&?[Y]:(Y=Z&((X=Y=>p(X,Y,Z))&?[X]:(X=Y&p(X,Y,Z)))))<=>((Y=Z=>((X=Z=>p(X,Y,Z))&?[X]:(X=Z&p(X,Y,Z))))&?[Y]:(Y=Z&((X=Z=>p(X,Y,Z))&?[X]:(X=Z&p(X,Y,Z))))))).

I obtain this result:

FATAL ERROR: BUG found in metis program:
cumulativeCounts: c1 = (+1.09861228867,-1.09861228867), c2 = (+1.09861228867,-1.38629436112)

I do not have much experience with metis or ATPs in general, so I cannot help much, but since metis itself is declaring a bug, I thought that I might be helpful to report.

Expanding simplify inference

Hi Joe,

With this problem:

$ cat impl-9.tptp
fof(a1, axiom, ((p => p) => q)).
fof(goal, conjecture, ((q => r) => r)).

I am getting this:

$ metis --show proof impl-9.tptp
fof(a1, axiom, ((p => p) => q)).
fof(goal, conjecture, ((q => r) => r)).
... 
fof(normalize_0_0, plain, (~ r & (~ q | r)),
    inference(canonicalize, [], [negate_0_0])).
fof(normalize_0_1, plain, (q), inference(canonicalize, [], [a1])).
fof(normalize_0_2, plain, ($false),
    inference(simplify, [], [normalize_0_0, normalize_0_1])).
...

The last result ($false) is clear but it expected based on other proofs
something else. What about printing proofs by expanding the simplify step,
like this example:

fof(a1, axiom, ((p => p) => q)).
fof(goal, conjecture, ((q => r) => r)).
... 
fof(normalize_0_0, plain, (~ r & (~ q | r)),
    inference(canonicalize, [], [negate_0_0])).
fof(normalize_0_1, plain, (~ q | r),
   inference(conjunct, [], normalize_0_0)).
fof(normalize_0_2, plain, (q), 
  inference(canonicalize, [], [a1])).
fof(normalize_0_3, plain, (r),
    inference(resolve, [$cnf(q)], [normalize_0_2, normalize_0_1])). 
fof(normalize_0_4, plain, ($false),
   inference(simplify, [], [normalize_0_3, normalize_0_0])).
...

Do we have any chance to expand the simplify inference?

Thanks,

CC'ing @asr

FATAL ERROR: BUG found in metis program: Active.simplify

Here is one more problem that triggers a bug in Metis. The error message states:

FATAL ERROR: BUG found in metis program:
Active.simplify: clause should have been simplified away

No proof when the conjecture is $true

Joe,

The output of the current version outputs nothing for true conjecture
like in the following file:

$ cat basic-01.tptp
fof(goal, conjecture, $true).
$ metis --version
metis 2.4 (release 20180810)
$ metis basic-01.tptp
% SZS status Theorem for basic-01.tptp

This used to be different. If we use a previous version we got something different
like the following (I'm using here my online-atps tool to call SystemOnTPTP, which
has Metis v2.4. Surely, an outdated version).

$ online-atps --version-atp=online-metis
Metis---2.4

And ...

$ online-atps --atp=online-metis test/prop-pack/problems/basic/basic-01.tptp
....
% SZS output start CNFRefutation for /tmp/SystemOnTPTPFormReply11095/SOT_A4iF9J
fof(goal, conjecture, ($true)).

fof(subgoal_0, plain, ($true), inference(strip, [], [goal])).

fof(negate_0_0, plain, (~ $true), inference(negate, [], [subgoal_0])).

fof(normalize_0_0, plain, ($false),
    inference(canonicalize, [], [negate_0_0])).

cnf(refute_0_0, plain, ($false),
    inference(canonicalize, [], [normalize_0_0])).
% SZS output end CNFRefutation for /tmp/SystemOnTPTPFormReply11095/SOT_A4iF9J
...

[ BUG ] Simplify erroneously deduces $false

Hi Joe,

Consider the following problem:

$ cat conj-01.tptp
fof(a1, axiom, p).
fof(a2, axiom, q).
fof(goal, conjecture, p & q).
$ metis --version
metis 2.3 (release 20171005)
$ metis --show proof conj-01.tptp
...
fof(a1, axiom, (p)).

fof(a2, axiom, (q)).
...
fof(normalize_0_0, plain, (~ p),
    inference(canonicalize, [], [negate_0_0])).
...

fof(normalize_1_0, plain, (~ q & p),
    inference(canonicalize, [], [negate_1_0])).

fof(normalize_1_1, plain, (q), inference(canonicalize, [], [a2])).

fof(normalize_1_2, plain, (p), inference(canonicalize, [], [a1])).

fof(normalize_1_3, plain, ($false),
    inference(simplify, [],
              [normalize_1_0, normalize_1_1, normalize_1_2])).

cnf(refute_1_0, plain, ($false),
    inference(canonicalize, [], [normalize_1_3])).
% SZS output end CNFRefutation for conj-01.tptp

Instead of using normalize_1_2, Metis should use for example normalize_0_0 to deduce $false in this example.

CC'ing @asr

Ordered paramodulation vs. superposition

Metis appears to implement the ordered paramodulation calculus. In the AR community, superposition, with its extra ordering restriction, is widely considered as a more efficient calculus. It is the calculus of E, SPASS, Vampire, Zipperposition, etc.

Is there a particular reason why Metis doesn't implement superposition?

If we were to provide a patch to perform superposition, would you potentially be interested in applying it upstream?

Jasmin & Martin

Fatal error on a big file

Running Metis on a 50 MB file from TPTP 6.4.0, I got the following fatal error:

$ cd TPTP/Axioms
$ metis MED002+0.ax

FATAL ERROR: metis failed:
error in TPTP file "MED002+0.ax" around line 1705619:
    mesh__activeMeSHYear(mesh__D007174,'2003') )).

%------------------------------------------------------------------------------
EOF inside a block comment

I could process the above file using other ATPs.

Version:

$ metis --version
metis 2.3 (release 20160714)

CC'ing @jonaprieto.

BUG found in metis program: Active.checkSaturated

When running Metis 2.3-20170925 (compiled with PolyML 5.7) on some problems, I obtain the error message:

FATAL ERROR: BUG found in metis program:
Active.checkSaturated

Two fatal errors on same TPTP problem, with non-default options

We recently updated Metis to 2.4 in Isabelle. Things ran smoothly on thousands of proof goals, but we ran into two regressions, where Metis suddenly gave "KeyMap.delete: element not found" errors. We translated one of the two problems to TPTP and modified metis.sml to use the same options as in Isabelle (see attachments), without which the bug didn't arise in a reasonable time. Playing with the options, we obtained a different error outcome ("Active.simplify: clause should have been simplified away"). Details on these errors and how to reproduce them can be found in the attached patch for metis.sml.

Let us know if you need any further information. This is not a showstopper for us.

Martin & Jasmin

bug.p.txt
metis.patch.txt

gilith / metis Goto Github PK

metis's Introduction

Metis Theorem Prover (Development Version)

Install

Build

Using the MLton compiler

Using the Poly/ML compiler

Using the Moscow ML compiler

Test

Troubleshoot

metis's People

Contributors

Stargazers

Watchers

Forkers

metis's Issues

Recommend Projects

Recommend Topics

Recommend Org