nick8325 / equinox Goto Github PK
View Code? Open in Web Editor NEWParadox model finder and equinox theorem prover for first-order logic.
License: MIT License
Paradox model finder and equinox theorem prover for first-order logic.
License: MIT License
[17 of 18] Compiling Equinox.FolSat ( Equinox/FolSat.hs, Equinox/FolSat.o )
Equinox/FolSat.hs:317:22: error:
• Could not deduce (Control.Monad.Fail.MonadFail Sat.S)
arising from a do statement
with the failable pattern ‘Left subs’
from the context: (Ord a, Num a, Show a)
bound by the inferred type of
findAllSubs :: (Ord a, Num a, Show a) =>
a -> Sat.S (Either [Map Symbol Con] (Bool, Set Symbol))
at Equinox/FolSat.hs:(305,12)-(327,42)
• In a stmt of a 'do' block: Left subs <- findAllSubs (i + 1)
In the expression:
do Sat.lift (showOne send (i + 1))
cs <- sequence [getModelValueValue v | v <- vs]
let sub = M.fromList (xs `zip` cs)
Sat.addClause [Sat.neg (v =? c) | (v, c) <- vs `zip` cs, c /= st]
....
In a stmt of a 'do' block:
if b then
do Sat.lift (showOne send (i + 1))
cs <- sequence [getModelValueValue v | v <- vs]
let sub = ...
....
else
do if i == 0 then do ... else do ...
|
317 | Left subs <- findAllSubs (i+1)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
make[1]: *** [Makefile:42: ../equinox] Error 1
Not sure what to do
Building equinox/paradox/etc. using the clang C++ compiler on Mac OS X 10.8 results in an error:
$ make
make Solver.or -C minisat/current-base
Compiling: Solver.or ( Solver.C )
clang: warning: argument unused during compilation: '-ffloat-store'
In file included from Solver.C:20:
In file included from ./Solver.h:65:
./VarOrder.h:88:1: warning: 'VarFilter' defined as a struct here but previously declared as a class [-Wmismatched-tags]
struct VarFilter {
^
./VarOrder.h:70:12: note: did you mean struct here?
friend class VarFilter;
^~~~~
struct
In file included from Solver.C:20:
./Solver.h:265:38: error: use of undeclared identifier 'Clause_new'
propagate_tmpbin = Clause_new(dummy);
^
./Solver.h:266:38: error: use of undeclared identifier 'Clause_new'
analyze_tmpbin = Clause_new(dummy);
^
./Solver.h:268:38: error: use of undeclared identifier 'Clause_new'
bwdsub_tmpunit = Clause_new(dummy);
^
./Solver.h:270:38: error: use of undeclared identifier 'Clause_new'
propagate_tmpempty = Clause_new(dummy);
^
Solver.C:89:23: error: use of undeclared identifier 'Clause_new'
Clause* c = Clause_new(ps, learnt);
^
Solver.C:879:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
else
^
Solver.C:910:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
else
^
3 warnings and 5 errors generated.
make[1]: *** [Solver.or] Error 1
make: *** [mk-minisat] Error 2
A solution it to use g++:
CXX=g++ make
[proceeds as expected]
For example, given the file refl.fof
:
fof(refl, conjecture, ! [X] : X = X).
Works:
$ equinox refl.fof
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
+++ PROBLEM: refl.fof
Reading 'refl.fof' ... OK
+++ SOLVING: refl.fof
#elt|#instances
+++ RESULT: Theorem
Fails:
$ equinox --time 10 refl.fof
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
equinox: <<loop>>
Even the --help
option fails:
$ equinox --help
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
Usage: equinox <option>* <file>*
<file> should be in TPTP format.
<option> can be any of the following:
equinox: <<loop>>
Tested with GHC 7.10.3 and 8.0.1.
CCing @jonaprieto
$ make
make Solver.or -C minisat/current-base
make[1]: Entering directory /Users/alama/sources/equinox/minisat/current-base' make[1]:
Solver.or' is up to date.
make[1]: Leaving directory /Users/alama/sources/equinox/minisat/current-base' make Prop.or -C minisat/current-base make[1]: Entering directory
/Users/alama/sources/equinox/minisat/current-base'
make[1]: Prop.or' is up to date. make[1]: Leaving directory
/Users/alama/sources/equinox/minisat/current-base'
make MiniSatWrapper.or -C instantiate
make[1]: Entering directory /Users/alama/sources/equinox/instantiate' make[1]:
MiniSatWrapper.or' is up to date.
make[1]: Leaving directory /Users/alama/sources/equinox/instantiate' make MiniSatInstantiateClause.or -C instantiate make[1]: Entering directory
/Users/alama/sources/equinox/instantiate'
make[1]: MiniSatInstantiateClause.or' is up to date. make[1]: Leaving directory
/Users/alama/sources/equinox/instantiate'
make -C Haskell
make[1]: Entering directory `/Users/alama/sources/equinox/Haskell'
ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded --make SmellySox/Main -o smellysox.exe
on the commandline:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
[ 2 of 19] Compiling SmellySox.Parser.Lextff ( SmellySox/Parser/Lextff.hs, SmellySox/Parser/Lextff.o )
templates/GenericTemplate.hs:119:22: Not in scope: `alexGetByte'
templates/GenericTemplate.hs:153:8: Not in scope: alexGetByte' make[1]: *** [smellysox.exe] Error 1 make[1]: Leaving directory
/Users/alama/sources/equinox/Haskell'
make: *** [mk-haskell] Error 2
When searching for models with paradox, I find that I often want to compare different models of a theory, specifically, models of different cardinalities. As it stands, though, this appears not to be possible with paradox without either (1) modifying the paradox sources, or (2) adding a premise to the theory saying that the domain size is at least N. Both of these are rather awkward; it seems better to me to support a minimum (and perhaps also maximum) domain size as a commandline parameter for paradox, similar to -n and -N for mace4.
On Mac OS X 10.10 with GCC (that is, not Apple's own compiler, but GNU C++), I'm not able to build equinox:
$ CXX=/sw/lib/gcc4.9/bin/g++-4 make
make Solver.or -C minisat/current-base
make[1]: Entering directory '/Users/alama/sources/equinox/minisat/current-base'
make[1]: 'Solver.or' is up to date.
make[1]: Leaving directory '/Users/alama/sources/equinox/minisat/current-base'
make Prop.or -C minisat/current-base
make[1]: Entering directory '/Users/alama/sources/equinox/minisat/current-base'
Compiling: Prop.or ( Prop.C )
In file included from Prop.h:23:0,
from Prop.C:20:
../mtl/Map.h: In constructor ‘Map<K, D, H, E>::Map(const H&, const E&)’:
../mtl/Map.h:87:41: warning: delegating constructors only available with -std=c++11 or -std=gnu++11
Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
^
../mtl/Map.h:87:50: error: mem-initializer for ‘Map<K, D, H, E>::hash’ follows constructor delegation
Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
^
../mtl/Map.h:87:61: error: mem-initializer for ‘Map<K, D, H, E>::equals’ follows constructor delegation
Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
^
Prop.C: In member function ‘Lit PropSolver::mkAnd(Lit, Lit)’:
Prop.C:93:45: warning: deprecated conversion from string constant to ‘char*’ [-Wwrite-strings]
logBinOp(logfile, v, f, g, " & ");
^
Prop.C: In member function ‘Lit PropSolver::mkEqu(Lit, Lit)’:
Prop.C:140:46: warning: deprecated conversion from string constant to ‘char*’ [-Wwrite-strings]
logBinOp(logfile, v, f, g, " == ");
^
../mtl/template.mk:61: recipe for target 'Prop.or' failed
make[1]: *** [Prop.or] Error 1
make[1]: Leaving directory '/Users/alama/sources/equinox/minisat/current-base'
Makefile:18: recipe for target 'mk-minisat' failed
make: *** [mk-minisat] Error 2
Here, /sw/lib/gcc4.9/bin/g++-4
is GNU G++ coming from the Fink project; it isn't the Apple-supplied C++ compiler.
Using equinox (commit cf20d54) I am unable to build Infinox. Here's a build log:
$ make
make Solver.or -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
make[1]: `Solver.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make Prop.or -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
make[1]: `Prop.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make MiniSatWrapper.or -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
make[1]: `MiniSatWrapper.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make MiniSatInstantiateClause.or -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
make[1]: `MiniSatInstantiateClause.or' is up to date.
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make -C Haskell
make[1]: Entering directory `/Users/alama/sources/equinox/Haskell'
ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded --make Paradox/Main.hs -o paradox
on the commandline:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
Parsek.hs:1:12:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded -threaded --make Equinox/Main.hs -o equinox
on the commandline:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
Parsek.hs:1:12:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
ghc -fglasgow-exts -O2 -static -threaded -main-is Infinox.Main.main --make Infinox.Main -o infinox
on the commandline:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
Infinox/Timeout.hs:1:12:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
Infinox/Timeout.hs:36:8:
Could not find module `System'
It is a member of the hidden package `haskell98-2.0.0.1'.
Use -v to see a list of the files searched for.
make[1]: *** [infinox.exe] Error 1
make[1]: Leaving directory `/Users/alama/sources/equinox/Haskell'
make: *** [mk-haskell] Error 2
Using ecc947c on Mac OS X 10.8, using GHC 7.4.2 coming from a fresh install of the Haskell Platform:
$ make
make Solver.or -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
Compiling: Solver.or ( Solver.C )
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make Prop.or -C minisat/current-base
make[1]: Entering directory `/Users/alama/sources/equinox/minisat/current-base'
Compiling: Prop.or ( Prop.C )
Prop.C: In function ‘void logBinOp(FILE*, Var, Lit, Lit, char*)’:
Prop.C:29: warning: format not a string literal and no format arguments
Prop.C:29: warning: format not a string literal and no format arguments
Prop.C: In member function ‘Lit PropSolver::mkAnd(Lit, Lit)’:
Prop.C:93: warning: deprecated conversion from string constant to ‘char*’
Prop.C: In member function ‘Lit PropSolver::mkEqu(Lit, Lit)’:
Prop.C:140: warning: deprecated conversion from string constant to ‘char*’
make[1]: Leaving directory `/Users/alama/sources/equinox/minisat/current-base'
make MiniSatWrapper.or -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
Making dependencies ...
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
Compiling: MiniSatWrapper.or ( MiniSatWrapper.C )
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make MiniSatInstantiateClause.or -C instantiate
make[1]: Entering directory `/Users/alama/sources/equinox/instantiate'
Compiling: MiniSatInstantiateClause.or ( MiniSatInstantiateClause.C )
MiniSatInstantiateClause.C: In member function ‘bool FOClause::instantiate(Solver&, int)’:
MiniSatInstantiateClause.C:239: warning: unused variable ‘ret’
make[1]: Leaving directory `/Users/alama/sources/equinox/instantiate'
make -C Haskell
make[1]: Entering directory `/Users/alama/sources/equinox/Haskell'
ghc -fglasgow-exts --make Sat.hs
on the commandline:
Warning: -fglasgow-exts is deprecated: Use individual extensions instead
Form.hs:32:8:
Could not find module `Control.Monad.State'
Perhaps you meant
Control.Monad.ST (from base)
Control.Monad.ST.Safe (from base)
Control.Monad.Fix (from base)
Use -v to see a list of the files searched for.
make[1]: *** [Sat.o] Error 1
make[1]: Leaving directory `/Users/alama/sources/equinox/Haskell'
make: *** [mk-haskell] Error 2
:(
I wanted to see a paradox model today!
Using Equinox version 5.0alpha 2010-06-29 (commit 9151a09, compiled with GHC 6.10.4), the attached problem is proved instantly:
$ time equinox regression.fof
Equinox, version 5.0alpha, 2010-06-29.
+++ PROBLEM: regression.fof
Reading 'regression.fof' ... OK
+++ SOLVING: regression.fof
#elt|m|#instances
12|P|....
12|L|1.>.
99|P|....
99|L|.L.1
190|P|L13.
+++ RESULT: Theorem
real 0m0.150s
user 0m0.142s
sys 0m0.008s
but using the upstream version the same problem is not proved in 10 minutes:
$ equinox --time 600 regression.fof
Equinox, version 6.0.1alpha, 2011-12-07, pre-release.
+++ PROBLEM: regression.fof
Reading 'regression.fof' ... OK
+++ SOLVING: regression.fof
...
*** TIMEOUT (600 seconds)
+++ RESULT: Timeout
Actually, I found the same kind of regression (proved in 5.0alpha 2010-06-29, not proved in upstream) in others TPTP problems, but the attached one is the simplest.
Paradox segfaults on Mac OS X 10.7, even with the latest ghc. The difficulty arises when dealing with "non-trivial" problems whose smallest countermodel has size, say, 5 or more. I don't know how to characterize the TPTP problems on which paradox crashes. All I can say is that when theories start to get a little complex, paradox becomes more likely to crash on Mac OS X. Even more strange, with a single theory paradox sometimes crashes and sometimes terminates.
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.4.1
$ paradox theorem36.p
Paradox, version 4.0, 2010-06-29.
+++ PROBLEM: theorem36.p
Reading 'theorem36.p' ... OK
+++ SOLVING: theorem36.p
domain size 1
domain size 2
domain size 3
domain size 4
domain size 5
domain size 6
domain size 7
Segmentation fault: 11
$ paradox theorem36.p
Paradox, version 4.0, 2010-06-29.
+++ PROBLEM: theorem36.p
Reading 'theorem36.p' ... OK
+++ SOLVING: theorem36.p
domain size 1
domain size 2
domain size 3
domain size 4
domain size 5
domain size 6
domain size 7
+++ RESULT: CounterSatisfiable
I attach the TPTP problem on which paradox exhibits this strange behavior.
% IndCon(x) -> Complete(x)
fof(individual_concepts_are_complete,conjecture,
(! [X,D] : ((object(X) & point(D)) =>
(individual_concept_wrt(X,D) => complete_wrt(X,D))))).
fof(tentative,axiom,
(? [X] : object(X))).
fof(pauls_principle,axiom,
(! [X] : (property(X) => ~(a_property_negation_of(X,X))))).
fof(theorem36_lemma1,lemma,
(! [D,X,F,G] : ((point(D) & object(X) & property(F) & property(G)) =>
(a_property_negation_of(G,F) =>
(ex1_wrt(F,X,D) | ex1_wrt(G,X,D)))))).
fof(theorem36_lemma2,lemma,
(! [D,X,F,G] : ((point(D) & object(X) & property(F) & property(G)) =>
(a_property_negation_of(G,F) => (ex1_wrt(G,X,D) <=> ~ex1_wrt(F,X,D)))))).
fof(theorem36_lemma3,lemma,
(! [X,F,G,Q,R,S]: ((object(X) & property(F) & property(G) & proposition(Q) & proposition(R) & proposition(S)) =>
((plug1(Q,F,X) & a_property_negation_of(G,F) & plug1(R,G,X) & is_a_disjunction_of(S,Q,R)) =>
( ( ! [D] : (point(D) => true_wrt(S,D))) => (! [W] : (object(W) => (world_wrt(W,d) => true_in_wrt(S,W,d))))))))).
fof(theorem36_lemma4,lemma,
(! [U,F,G,P,Q,W,X] : ((object(X) & object(U) & property(F) & object(W) & property(G) & proposition(P) & proposition(Q)) =>
((a_property_negation_of(G,F) & plug1(P,F,U) & plug1(Q,G,U) & ex1_wrt(o,U,d) & world_wrt(W,d) & ex1_wrt(c,X,d)) =>
(((true_in_wrt(P,W,d) | true_in_wrt(Q,W,d)) & realizes_in_wrt(U,X,W,d)) =>
(enc_wrt(X,F,d) | enc_wrt(X,G,d))))))).
% (! [X,H,R] : ((object(X) & property(H) & proposition(R)) =>
% ((ex1_wrt(c,X,d) & plug1(R,H,U)) => (true_in_wrt(R,W,D) <=> enc_wrt(X,H,D)))))) =>
fof(sort_realizes_in_wrt,axiom,
( ! [U,X,W,D] : ( realizes_in_wrt(U,X,W,D) => (object(U) & object(X) & object(W) & point(D))))).
fof(sort_individual_concept,axiom,
( ! [X,D] : (individual_concept_wrt(X,D) => (point(D) & object(X))))).
fof(sort_appears_in_wrt,axiom,
(! [X,W,D] : (appears_in_wrt(X,W,D) => (point(D) & object(X) & object(W))))).
% Definition of IndividualConcept(x)
fof(def_individual_concept_wrt,axiom,
(! [X,D] : ((object(X) & point(D)) => (individual_concept_wrt(X,D) <=>
(ex1_wrt(c,X,D) & (? [W] : (object(W) & world_wrt(W,D) & appears_in_wrt(X,W,D)))))))).
% Definition of AppearanceAt
fof(def_appears_in_wrt,axiom,
(! [D,X,W] : ((point(D) & object(X) & object(W)) =>
(appears_in_wrt(X,W,D) <=> (ex1_wrt(c,X,D) & world_wrt(W,D) &
(? [U] : (object(U) & ex1_wrt(o,U,D) & realizes_in_wrt(U,X,W,D)))))))).
% Definition of RealizesInAt
fof(def_realizes_in_wrt,axiom,
(! [D,U,X,W,P] : ((point(D) & object(U) & object(X) & object(W) & proposition(P)) =>
(realizes_in_wrt(U,X,W,D) <=> (ex1_wrt(o,U,D) & ex1_wrt(c,X,D) & world_wrt(W,D) &
(! [F] : ((property(F) =>
(plug1(P,F,U) =>
(true_in_wrt(P,W,D) <=> enc_wrt(X,F,D))))))))))).
fof(existence_proposition_plug1,axiom,
(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
% from principia/includes/propositions.ax
fof(proposition_plug1_truth,axiom,
(! [X,F,P] : ((object(X) & property(F) & proposition(P)) =>
(plug1(P,F,X) =>
(! [D] : (point(D) => (true_wrt(P,D) <=> ex1_wrt(F,X,D)))))))).
% Definition of Complete(x)
fof(def_complete,axiom,
( ! [X,D] : ((object(X) & point(D)) =>
(complete_wrt(X,D) <=> (! [F,G] : ((property(F) & property(G) & a_property_negation_of(G,F)) =>
(enc_wrt(X,F,D) | enc_wrt(X,G,D)))))))).
% There is at least one negation of each property.
fof(property_negation,axiom,
(! [F] : (property(F) => (? [G] : (property(G) & a_property_negation_of(G,F)))))).
% Axiom for property negation
fof(meaning_postulate_a_property_negation_of,axiom,
(! [F,G] : ((property(F) & property(G)) =>
(a_property_negation_of(G,F) <=>
(! [X,D] : ((object(X) & point(D)) =>
(ex1_wrt(G,X,D) <=> ~ex1_wrt(F,X,D)))))))).
fof(property_negation_sorting,axiom,
(! [G,F] : (a_property_negation_of(G,F) => (property(G) & property(F))))).
% Principle from World Theory (Kripke Principle)
fof(necessary_truth_implies_truth_at_every_world,lemma,
(! [P] : ((proposition(P) =>
(! [D] : (point(D) => true_wrt(P,D)) =>
(! [W]: (object(W) => (world_wrt(W,d) => true_in_wrt(P,W,d))))))))).
fof(existence_a_disjunction_of,axiom,
(! [P,Q] : ((proposition(P) & proposition(Q)) =>
(? [R] : (proposition(R) & is_a_disjunction_of(R,P,Q)))))).
fof(axiom_is_a_disjunction_of,axiom,
(! [P,Q,R] : ((proposition(P) & proposition(Q) & proposition(R)) =>
(is_a_disjunction_of(R,P,Q) <=>
(! [D] : (point(D) => (true_wrt(R,D) <=> (true_wrt(P,D) | true_wrt(Q,D))))))))).
fof(is_a_disjunction_of_sorting,axiom,
(! [P,Q,R] : (is_a_disjunction_of(R,P,Q) => (proposition(P) & proposition(Q) & proposition(R))))).
fof(is_a_disjunction_of_distributes,axiom,
(! [P,Q,R] : ((proposition(P) & proposition(Q) & proposition(R)) =>
(is_a_disjunction_of(R,P,Q) =>
(! [W] : (object(W) =>
(world_wrt(W,d) =>
(true_in_wrt(R,W,d) <=> (true_in_wrt(P,W,d) | true_in_wrt(Q,W,d)))))))))).
% ^ we may need to turn this into a biconditional
% Distinguished Elements.
fof(distinguished_property_e,axiom,property(e)).
fof(being_a_concept_is_being_abstract,axiom,c=a).
fof(distinctness_o_e,axiom,o!=e).
fof(distinctness_a_e,axiom,a!=e).
fof(distinctness_o_a,axiom,o!=a).
% Defined Notions
fof(def_o_wrt,axiom,
(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(def_a_wrt,axiom,
(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~(? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(def_encp_wrt,axiom,
(! [X,P,D] : ((object(X) & proposition(P) & point(D)) =>
(encp_wrt(X,P,D) <=> (? [F] : (property(F) & vac(F,P) & enc_wrt(X,F,D))))))).
fof(def_true_in_wrt,axiom,
(! [P,X,D] : ((proposition(P) & object(X) & point(D)) =>
(true_in_wrt(P,X,D) <=> encp_wrt(X,P,D))))).
% Sorting Principles
fof(sort_o,axiom,property(o)).
fof(sort_a,axiom,property(a)).
fof(sort_true_in_wrt,axiom,
(! [P,X,D] : (true_in_wrt(P,X,D) => (proposition(P) & object(X) & point(D))))).
% Distinguished Elements
fof(distinguished_point_d,axiom,point(d)).
% Sorting on Primitive Notions
fof(sort_properties_not_points,axiom,
(! [X] : (property(X) => ~point(X)))).
fof(sort_properties_not_objects,axiom,
(! [X] : (property(X) => ~object(X)))).
fof(sort_objects_not_points,axiom,
(! [X] : (object(X) => ~point(X)))).
%% fof(sort_propositions_not_points_objects_or_properties,axiom,
%% (! [X] : (proposition(X) => ~(point(X) | object(X) | property(X))))).
fof(sort_ex1_wrt,axiom,
(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & object(X) & point(D))))).
fof(sort_enc_wrt,axiom,
(! [X,F,D] : (enc_wrt(X,F,D) => (object(X) & property(F) & point(D))))).
fof(sort_true_wrt,axiom,
(! [P,D] : (true_wrt(P,D) => (proposition(P) & point(D))))).
fof(sort_true_in_wrt,axiom,
(! [P,W,D] : (true_in_wrt(P,W,D) => (proposition(P) & object(W) & point(D))))).
fof(sort_individual_concept_wrt,axiom,
(! [X,D] : (individual_concept_wrt(X,D) => (object(X) & point(D))))).
% Logical Axioms
fof(rigidity_of_encoding,axiom,
(! [X,F] : ((object(X) & property(F)) =>
((? [D] : (point(D) & enc_wrt(X,F,D))) =>
(! [D] : (point(D) => enc_wrt(X,F,D))))))).
Some problems cause assertions to fail in MiniSatInstantiateClause.cc
:
bug_clausify.tptp
incomplete4.tptp
incomplete5.tptp
The instantiation code was previously compiled with -DNDEBUG
which meant that the failures were ignored.
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.