More complex blocks world axiomatization

%-------------------------------------------------------------------------- % File  : PLA001-0 : TPTP v7.2.0. Released v1.0.0. % Domain  : Planning (Blocks world) % Axioms  : Blocks world axioms %--------------------------------------------------------------------------

cnf(and_definition,axiom,

   ( holds(and(X,Y),State)
   | ~ holds(X,State)
   | ~ holds(Y,State) )).

cnf(pickup_1,axiom,

   ( holds(holding(X),do(pickup(X),State))
   | ~ holds(empty,State)
   | ~ holds(clear(X),State)
   | ~ differ(X,table) )).

cnf(pickup_2,axiom,

   ( holds(clear(Y),do(pickup(X),State))
   | ~ holds(on(X,Y),State)
   | ~ holds(clear(X),State)
   | ~ holds(empty,State) )).

cnf(pickup_3,axiom,

   ( holds(on(X,Y),do(pickup(Z),State))
   | ~ holds(on(X,Y),State)
   | ~ differ(X,Z) )).

cnf(pickup_4,axiom,

   ( holds(clear(X),do(pickup(Z),State))
   | ~ holds(clear(X),State)
   | ~ differ(X,Z) )).

cnf(putdown_1,axiom,

   ( holds(empty,do(putdown(X,Y),State))
   | ~ holds(holding(X),State)
   | ~ holds(clear(Y),State) )).

cnf(putdown_2,axiom,

   ( holds(on(X,Y),do(putdown(X,Y),State))
   | ~ holds(holding(X),State)
   | ~ holds(clear(Y),State) )).

cnf(putdown_3,axiom,

   ( holds(clear(X),do(putdown(X,Y),State))
   | ~ holds(holding(X),State)
   | ~ holds(clear(Y),State) )).

cnf(putdown_4,axiom,

   ( holds(on(X,Y),do(putdown(Z,W),State))
   | ~ holds(on(X,Y),State) )).

cnf(putdown_5,axiom,

   ( holds(clear(Z),do(putdown(X,Y),State))
   | ~ holds(clear(Z),State)
   | ~ differ(Z,Y) )).
   

%-------------------------------------------------------------------------- % File  : PLA001-1 : TPTP v7.2.0. Released v1.0.0. % Domain  : Planning (Blocks world) % Axioms  : Blocks world difference axioms for 4 blocks %--------------------------------------------------------------------------

cnf(symmetry_of_differ,axiom,

   ( differ(X,Y)
   | ~ differ(Y,X) )).

cnf(differ_a_b,axiom,

   ( differ(a,b) )).

cnf(differ_a_c,axiom,

   ( differ(a,c) )).

cnf(differ_a_d,axiom,

   ( differ(a,d) )).

cnf(differ_a_table,axiom,

   ( differ(a,table) )).

cnf(differ_b_c,axiom,

   ( differ(b,c) )).

cnf(differ_b_d,axiom,

   ( differ(b,d) )).

cnf(differ_b_table,axiom,

   ( differ(b,table) )).

cnf(differ_c_d,axiom,

   ( differ(c,d) )).

cnf(differ_c_table,axiom,

   ( differ(c,table) )).

cnf(differ_d_table,axiom,

   ( differ(d,table) )).

%----Initial configuration: % % c % a b d % -------------------------------

cnf(initial_state1,axiom,

   ( holds(on(a,table),s0) )).

cnf(initial_state2,axiom,

   ( holds(on(b,table),s0) )).

cnf(initial_state3,axiom,

   ( holds(on(c,d),s0) )).

cnf(initial_state4,axiom,

   ( holds(on(d,table),s0) )).

cnf(initial_state5,axiom,

   ( holds(clear(a),s0) )).

cnf(initial_state6,axiom,

   ( holds(clear(b),s0) )).

cnf(initial_state7,axiom,

   ( holds(clear(c),s0) )).

cnf(initial_state8,axiom,

   ( holds(empty,s0) )).

%----Table is always clear

cnf(clear_table,axiom,

   ( holds(clear(table),State) )).
 

%-------------------------------------------------------------------------- % % questions: % % the second etc are commented out: try also these (remember to outcomment others) % % % % -----------------------------------------------------------------------

%cnf(prove_CBA,negated_conjecture,
%  ( ~ holds(on(d,a),State) )).
  
cnf(prove_CBA,negated_conjecture,
  ( ~ holds(on(d,a),State) | $ans(State))).   

% this one asks to construct this tower (which could be on table or on top of other blocks): % % c % b % a % % proving this will take ca 8 secs, during which a prover tries out several search strategies sequentially

% cnf(prove_CBA,negated_conjecture, % ( ~ holds(and(on(c,b),on(b,a)),State) )).

% this one asks to construct these towers (but, they could be also on top of each other!): % % c d % a b

% cnf(prove_CA_DB,negated_conjecture, % ( ~ holds(and(on(c,a),on(d,b)),State) )).

% this one asks to construct % % d % c

% cnf(prove_DC,negated_conjecture, % ( ~ holds(on(d,c),State) )).