Simple axiomatization of the blocks world - Redigeerimiste ajalugu

Tammet – 17. aprill 2020, kell 07:01

2020-04-17T07:01:18Z

←Vanem redaktsioon		Redaktsioon: 17. aprill 2020, kell 09:01
205. rida:		205. rida:
	% -holds(on(b,a),State) \| -holds(on(c,b),State) \| $ans(State)).		% -holds(on(b,a),State) \| -holds(on(c,b),State) \| $ans(State)).

	<pre>		</pre>

Tammet – 17. aprill 2020, kell 06:42

2020-04-17T06:42:23Z

←Vanem redaktsioon		Redaktsioon: 17. aprill 2020, kell 08:42
88. rida:		88. rida:
	%		%
	% These say what conditions must hold for the robot hand to pick		% These say what conditions must hold for the robot hand to pick
	% up ~~or put down~~ something and what happens to the state when the action		% up something and what happens to the state when the action
	% is done.		% is done.
	%		%

Tammet – 17. aprill 2020, kell 05:12

2020-04-17T05:12:38Z

←Vanem redaktsioon		Redaktsioon: 17. aprill 2020, kell 07:12
1. rida:		1. rida:
	<pre>		<pre>
	% ----- initial situation s0 ------		% ----- initial situation s0 ------
			%
			% blocks on table layed out thus:
	%		%
	% c		% c
	% a b d		% a b d
	% ------------------------------		% ------------------------------
			%
			% in "holds(X,Y)" X says something X about the blocks world
			% and Y describes the state we have arrived to via robot actions from the original state
			%
			% s0 is our name for the initial state.
			%
			% "clear(X)" means that someting can be put on X
			% "holds(empty,Y)" means that the robot hand is empty in state Y.
			% ---------------------------------------------------------------


	holds(on(a,table),s0).		holds(on(a,table),s0).
26. rida:		38. rida:

	% ---- difference of objects -----		% ---- difference of objects -----
			%
			% By default we do not know that "a" and "b" denote different blocks.
			% Could well be that they are two labels of the same block.
			%
			% Instead of "differ(X,Y)" we could axiomatize that they are not equal, using
			% "X != Y" but equality allows to derive a lot of additional stuff, bogging down
			% proof search. Here we use a simpler axiomatizon of being different.
			%
			% Difference of "a" and "b" etc is used both in the robot arm axioms
			% and the frame axioms in the following
			%
			% ---------------------------------


51. rida:		75. rida:
	differ(d,table).		differ(d,table).

			% ------- logic additionally encoded in terms -----
			% we are not using a special "and" function, but if we wanted to,
			% this would be one way to say it:
			%
	%holds(and(X,Y),State)		%holds(and(X,Y),State)
	% \| -holds(X,State)		% \| -holds(X,State)
	% \| -holds(Y,State).		% \| -holds(Y,State).
			% -----------------------------------------------


	% ----- pickup rules ------		% ----- pickup rules ------
			%
			% These say what conditions must hold for the robot hand to pick
			% up or put down something and what happens to the state when the action
			% is done.
			%
			% ---------------------------

	holds(holding(X),do(pickup(X),State))		holds(holding(X),do(pickup(X),State))
67. rida:		103. rida:
	\| -holds(empty,State).		\| -holds(empty,State).

			% -----------------------
	% frame axioms for pickup		% frame axioms for pickup
			%
			% Saying that if something is picked up, most of the things which did
			% hold in the previous state will still hold in the new state
			%
			% Notice the use of "differ".
			% -----------------------


	holds(on(X,Y),do(pickup(Z),State))		holds(on(X,Y),do(pickup(Z),State))
78. rida:		122. rida:

	% ---- putdown rules -----		% ---- putdown rules -----
			%
			% Similarly to picking up a block, what is required for putting it down
			% and what happens to the state after putting down.
			%
			% The first rule states that the robot hand will be empty after
			% it puts down something
			%
			% ---------------------

	holds(empty,do(putdown(X,Y),State))		holds(empty,do(putdown(X,Y),State))
91. rida:		143. rida:
	\| -holds(clear(Y),State).		\| -holds(clear(Y),State).

	% ---- ~~a few minimal~~ frame axioms for putdown -----		% ---- frame axioms for putdown -----

	holds(on(X,Y),do(putdown(Z,W),State))		holds(on(X,Y),do(putdown(Z,W),State))
107. rida:		159. rida:
	% * create your own goals: see what can be achieved in sensible time and what not.		% * create your own goals: see what can be achieved in sensible time and what not.
	%		%
			% Solving queries in the block world is surprisingly hard:
			% there are lot of possible action paths the robot hand could take
			% and there are a lot of axioms which have to be checked and used.
			%
			% If you wanted to do real planning quickly in a formalization like this,
			% you'd need a specialized search strategy plus possibly special mechanisms
			% for ignoring some potential paths of actions and some sequences of
			% derivations from rules: it nthis way the search could be made fast.
			% The default search strategies of provers are pretty bad for these
			% kinds of problems.
			%
	% -------------------------------		% -------------------------------

	% first goal:		% first goal: try to put "b" on "a".
	%		%
	% b		% b
	% a		% a
			%
			% Notice we do not require that "a" is on "table": it could
			% well be sitting on a block "c".

			% this version simply asks whether a sequence of required moves
			% exists but does not explicitly print it out as an answer:
			%
	% -holds(on(b,a),State).		% -holds(on(b,a),State).
	%
	% this version gives the required moves collected into State:		% this version gives the required moves collected into State,
	%		% as required for planning the actions:

	-holds(on(b,a),State) \| $ans(State).		-holds(on(b,a),State) \| $ans(State).

Tammet – 16. aprill 2020, kell 21:51

2020-04-16T21:51:59Z

←Vanem redaktsioon		Redaktsioon: 16. aprill 2020, kell 23:51
1. rida:		1. rida:
			<pre>
	% ----- initial situation s0 ------		% ----- initial situation s0 ------
	%		%
135. rida:		135. rida:
	% cnf(prove,negated_conjecture,		% cnf(prove,negated_conjecture,
	% -holds(on(b,a),State) \| -holds(on(c,b),State) \| $ans(State)).		% -holds(on(b,a),State) \| -holds(on(c,b),State) \| $ans(State)).

			<pre>

Tammet: Uus lehekülg: ' % ----- initial situation s0 ------ % % c % a b d % ------------------------------ holds(on(a,table),s0). holds(on(b,table),s0). holds(on(c,d),s0). holds(o...'

2020-04-16T21:44:56Z

Uus lehekülg: ' % ----- initial situation s0 ------ % % c % a b d % ------------------------------ holds(on(a,table),s0). holds(on(b,table),s0). holds(on(c,d),s0). holds(o...'

Uus lehekülg

% ----- initial situation s0 ------
%
% c
% a b d
% ------------------------------

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

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

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

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

holds(clear(a),s0).

holds(clear(b),s0).

holds(clear(c),s0).

holds(empty,s0).

holds(clear(table),State).

% ---- difference of objects -----

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

differ(a,b).

differ(a,c).

differ(a,d).

differ(a,table).

differ(b,c).

differ(b,d).

differ(b,table).

differ(c,d).

differ(c,table).

differ(d,table).

%holds(and(X,Y),State)
% | -holds(X,State)
% | -holds(Y,State).

% ----- pickup rules ------

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

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

% frame axioms for pickup

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

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

% ---- putdown rules -----

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

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

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

% ---- a few minimal frame axioms for putdown -----

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

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

% ----- queries -----------------
%
% first run the uncommented query and then:
%
% * try out the others: uncomment one and comment out others
% * create your own goals: see what can be achieved in sensible time and what not.
%
% -------------------------------

% first goal:
%
% b
% a

% -holds(on(b,a),State).
%
% this version gives the required moves collected into State:
%

-holds(on(b,a),State) | $ans(State).

% second goal:
%
% c
% b
% a

% -holds(on(b,a),State) | -holds(on(c,b),State).
%
% this version gives the required moves collected into State (over a minute to find proof!)
%
%
% cnf(prove,negated_conjecture,
% -holds(on(b,a),State) | -holds(on(c,b),State) | $ans(State)).