search

nick8325 / equinox

Paradox model finder and equinox theorem prover for first-order logic.
MIT License
19 stars 4 forks source link

paradox segfaults on Mac OS X 10.7 #7

Closed jessealama closed 7 years ago

jessealama commented 11 years ago

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))))))).
nick8325 commented 11 years ago

This is very mysterious! I'm afraid I couldn't reproduce it myself. Does it still occur for you on GHC 7.6?

If it's still a problem for you, the only thing I can think of is that it could be a problem with the FFI interface to MiniSat. You could try going into Haskell/Sat.hs and changing "unsafe" to "safe" in the declarations of s_clause, s_clause1, s_clause2, s_clause3, s_solve and s_simplify. But I'm doubtful that that will help.

nick8325 commented 7 years ago

It turns out we were using an old version of MiniSat which did an out-of-bounds array read! Paradox is now updated to the latest version of MiniSat which should hopefully fix the problem.