http://www.lambda.ee/w/index.php?action=history&feed=atom&title=PLA001-0.ax 2026-11-07T00:39:36Z Selle lehekülje redigeerimiste ajalugu MediaWiki 1.43.11 http://www.lambda.ee/w/index.php?title=PLA001-0.ax&diff=15673&oldid=prev 2019-03-20T09:33:42Z

<p>Uus lehekülg: &#039;&lt;pre&gt; %-------------------------------------------------------------------------- % File : PLA001-0 : TPTP v7.2.0. Released v1.0.0. % Domain : Planning (Blocks world) % Axi...&#039;</p> <p><b>Uus lehekülg</b></p><div>&lt;pre&gt;<br /> %--------------------------------------------------------------------------<br /> % File : PLA001-0 : TPTP v7.2.0. Released v1.0.0.<br /> % Domain : Planning (Blocks world)<br /> % Axioms : Blocks world axioms<br /> % Version : [SE94] axioms.<br /> % English :<br /> <br /> % Refs : [Sus73] Sussman (1973), A Computational Model of Skill Acquisi<br /> % : [SE94] Segre &amp; Elkan (1994), A High-Performance Explanation-B<br /> % Source : [SE94]<br /> % Names :<br /> <br /> % Status : Satisfiable<br /> % Syntax : Number of clauses : 10 ( 0 non-Horn; 0 unit; 8 RR)<br /> % Number of atoms : 31 ( 0 equality)<br /> % Maximal clause size : 4 ( 3 average)<br /> % Number of predicates : 2 ( 0 propositional; 2-2 arity)<br /> % Number of functors : 9 ( 2 constant; 0-2 arity)<br /> % Number of variables : 33 ( 3 singleton)<br /> % Maximal term depth : 3 ( 2 average)<br /> % SPC : <br /> <br /> % Comments : The axioms are a reconstruction of the situation calculus<br /> % blocks world as in [Sus73].<br /> %--------------------------------------------------------------------------<br /> cnf(and_definition,axiom,<br /> ( holds(and(X,Y),State)<br /> | ~ holds(X,State)<br /> | ~ holds(Y,State) )).<br /> <br /> cnf(pickup_1,axiom,<br /> ( holds(holding(X),do(pickup(X),State))<br /> | ~ holds(empty,State)<br /> | ~ holds(clear(X),State)<br /> | ~ differ(X,table) )).<br /> <br /> cnf(pickup_2,axiom,<br /> ( holds(clear(Y),do(pickup(X),State))<br /> | ~ holds(on(X,Y),State)<br /> | ~ holds(clear(X),State)<br /> | ~ holds(empty,State) )).<br /> <br /> cnf(pickup_3,axiom,<br /> ( holds(on(X,Y),do(pickup(Z),State))<br /> | ~ holds(on(X,Y),State)<br /> | ~ differ(X,Z) )).<br /> <br /> cnf(pickup_4,axiom,<br /> ( holds(clear(X),do(pickup(Z),State))<br /> | ~ holds(clear(X),State)<br /> | ~ differ(X,Z) )).<br /> <br /> cnf(putdown_1,axiom,<br /> ( holds(empty,do(putdown(X,Y),State))<br /> | ~ holds(holding(X),State)<br /> | ~ holds(clear(Y),State) )).<br /> <br /> cnf(putdown_2,axiom,<br /> ( holds(on(X,Y),do(putdown(X,Y),State))<br /> | ~ holds(holding(X),State)<br /> | ~ holds(clear(Y),State) )).<br /> <br /> cnf(putdown_3,axiom,<br /> ( holds(clear(X),do(putdown(X,Y),State))<br /> | ~ holds(holding(X),State)<br /> | ~ holds(clear(Y),State) )).<br /> <br /> cnf(putdown_4,axiom,<br /> ( holds(on(X,Y),do(putdown(Z,W),State))<br /> | ~ holds(on(X,Y),State) )).<br /> <br /> cnf(putdown_5,axiom,<br /> ( holds(clear(Z),do(putdown(X,Y),State))<br /> | ~ holds(clear(Z),State)<br /> | ~ differ(Z,Y) )).<br /> <br /> %--------------------------------------------------------------------------<br /> <br /> &lt;/pre&gt;</div>

Tammet