gilith / metis Goto Github PK
View Code? Open in Web Editor NEWAn automatic theorem prover for first order logic with equality
Home Page: http://www.gilith.com/metis/
License: MIT License
An automatic theorem prover for first order logic with equality
Home Page: http://www.gilith.com/metis/
License: MIT License
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
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
...
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
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.
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
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
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
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
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.
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
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.