http://www.lambda.ee/w/index.php?action=history&feed=atom&title=PLA005-1.p 2026-11-07T02:07:54Z Selle lehekülje redigeerimiste ajalugu MediaWiki 1.43.11 http://www.lambda.ee/w/index.php?title=PLA005-1.p&diff=15678&oldid=prev 2019-03-20T09:37:21Z

<p>Uus lehekülg: &#039;&lt;pre&gt; %-------------------------------------------------------------------------- % File : PLA005-1 : TPTP v7.2.0. Released v1.1.0. % Domain : Planning (Blocks world) % Pro...&#039;</p> <p><b>Uus lehekülg</b></p><div>&lt;pre&gt;<br /> %--------------------------------------------------------------------------<br /> % File : PLA005-1 : TPTP v7.2.0. Released v1.1.0.<br /> % Domain : Planning (Blocks world)<br /> % Problem : Block C on A and D on B<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 : - [SE94]<br /> <br /> % Status : Unsatisfiable<br /> % Rating : 0.25 v6.2.0, 0.33 v6.1.0, 0.57 v6.0.0, 0.44 v5.5.0, 0.50 v5.4.0, 0.56 v5.3.0, 0.60 v5.2.0, 0.69 v5.1.0, 0.56 v5.0.0, 0.53 v4.0.1, 0.57 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.14 v2.5.0, 0.43 v2.4.0, 0.43 v2.3.0, 0.29 v2.2.1, 0.22 v2.2.0, 0.33 v2.1.0, 0.43 v2.0.0<br /> % Syntax : Number of clauses : 31 ( 0 non-Horn; 20 unit; 28 RR)<br /> % Number of atoms : 53 ( 0 equality)<br /> % Maximal clause size : 4 ( 2 average)<br /> % Number of predicates : 2 ( 0 propositional; 2-2 arity)<br /> % Number of functors : 14 ( 7 constant; 0-2 arity)<br /> % Number of variables : 37 ( 5 singleton)<br /> % Maximal term depth : 3 ( 1 average)<br /> % SPC : CNF_UNS_RFO_NEQ_HRN<br /> <br /> % Comments : The axioms are a reconstruction of the situation calculus<br /> % blocks world as in [Sus73].<br /> %--------------------------------------------------------------------------<br /> %----Include Blocks world axioms<br /> include(&#039;Axioms/PLA001-0.ax&#039;).<br /> %----Include Blocks world difference axioms for 4 blocks<br /> include(&#039;Axioms/PLA001-1.ax&#039;).<br /> %--------------------------------------------------------------------------<br /> cnf(prove_CA_DB,negated_conjecture,<br /> ( ~ holds(and(on(c,a),on(d,b)),State) )).<br /> <br /> %--------------------------------------------------------------------------<br /> <br /> &lt;/pre&gt;</div>

Tammet