Tammet – 16. aprill 2020, kell 21:47

2020-04-16T21:47:15Z

←Vanem redaktsioon		Redaktsioon: 16. aprill 2020, kell 23:47
142. rida:		142. rida:
	% -----------------------------------------------------------------------		% -----------------------------------------------------------------------

	%cnf(~~prove_CBA~~,negated_conjecture,		%cnf(prove_DA,negated_conjecture,
	% ( ~ holds(on(d,a),State) )).		% ( ~ holds(on(d,a),State) )).

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

Tammet – 16. aprill 2020, kell 21:45

2020-04-16T21:45:56Z

←Vanem redaktsioon		Redaktsioon: 16. aprill 2020, kell 23:45
1. rida:		1. rida:
			<pre>
	%--------------------------------------------------------------------------		%--------------------------------------------------------------------------
	% File : PLA001-0 : TPTP v7.2.0. Released v1.0.0.		% File : PLA001-0 : TPTP v7.2.0. Released v1.0.0.
180. rida:		180. rida:
	% cnf(prove_DC,negated_conjecture,		% cnf(prove_DC,negated_conjecture,
	% ( ~ holds(on(d,c),State) )).		% ( ~ holds(on(d,c),State) )).
			</pre>

Tammet – 16. aprill 2020, kell 21:45

2020-04-16T21:45:39Z

←Vanem redaktsioon		Redaktsioon: 16. aprill 2020, kell 23:45
1. rida:		1. rida:

	%--------------------------------------------------------------------------		%--------------------------------------------------------------------------
	% File : PLA001-0 : TPTP v7.2.0. Released v1.0.0.		% File : PLA001-0 : TPTP v7.2.0. Released v1.0.0.

Tammet: Uus lehekülg: '%-------------------------------------------------------------------------- % File : PLA001-0 : TPTP v7.2.0. Released v1.0.0. % Domain : Planning (Blocks world) % Axioms...'

2020-04-16T21:45:29Z

Uus lehekülg: '%-------------------------------------------------------------------------- % File : PLA001-0 : TPTP v7.2.0. Released v1.0.0. % Domain : Planning (Blocks world) % Axioms...'

Uus lehekülg

%--------------------------------------------------------------------------
% 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) )).

More complex blocks world axiomatization - Redigeerimiste ajalugu

Tammet – 16. aprill 2020, kell 21:47

Tammet – 16. aprill 2020, kell 21:45

Tammet – 16. aprill 2020, kell 21:45

Tammet: Uus lehekülg: '%-------------------------------------------------------------------------- % File : PLA001-0 : TPTP v7.2.0. Released v1.0.0. % Domain : Planning (Blocks world) % Axioms...'