, . ; . , ( , ). , Prolog . : ; , . , , , . ,
v ~
" " , . .
~. , "not" ().
S. , "and" ().
v. , "" ().
=>. , "implies" ( ).
, "not" , "and", "or" "implies".
: , , , , . , , , (.. ). : , , -
23,
, , , ( ). , , .
. , , : ( => b) S ( => ) => ( => )
: " b , ".
, , , . , , , :
|
|
|
[p i v p j v...) & Iqi v qj v,.,) (r i v v...) 4...
, q . ( , ), . (pi v p; v...) . ( ). , , , . :
( => ) [ =>) -> [ => )
:
-((a =>b) 6 (=>) -> ( =>
, .
1. => - v .
2. --{ v ) ~ & -.
3. -{ & ) - v -,
4. ~(~) .
1 , :
- (- [ [ => & ( => )) v ( => ))
2 4 : { -> ) ( ] 5 ~( = > !
1, : (~ v b) t (-b v ) -(-a v )
2, , :
(-a v ) & [~ v ) & & -
: [~ v b), (~b v ), , --. .
, , , -. , :
v y - v z
584 II. Prolog
- , a Y Z - . , , :
Y v 2
, . , !Y v Z) , . , . " " ( "nil"), , . nil , :
X ~
, , .
. 23.5 , .
. 23.5. (a => ) i ( => ) => ( "> ) . . ,
|
|
|
23.10 , ; , . , . , , .
>
, 1 2, ,
() 1,; 1 ~ - 2,
"*' ~"
1 ( ), ~ 2 ( ) : v
23.10,
% Prolog
:- dynamic clause/1, done/3.
23. 585
% %
[ clause! X), clause! -X) ] >
[ write['Contradiction found') stop]. %
[ clause! ), in(P, ), in(-P, C] ] >
[ retract! C) ]. t
%
[ clause! ], delete! P, C, CD, in (P, CD ]- >
[ replace! clause! C), clause! CD) ]. % ,
[ clause! P), clause! ), delete! -, , Cl), net done (, , ) ] >
[ assert! clause! CD), assert! done [ P, , )) ].
% ,
[ clause! -P), clause! ), delete! , , CD, not done,- -P, , ) ] >
[ assert! clause! CD), assert! done (-P, C, P)) ]. % , [ clause(Cl), delete I P, Cl, Cft),
clause[C2)r delete! -P, C2, CB), not done{ C1,C2,P) ] -> [ assert! clause[CA v CB)), assert! done[ Cl, C2, P)) ].
% :
[]-- > [ writeCNot contradiction1), stop].
* delete! P, E, £1)
% 1
delete! X, X v Y, Y).
delete! X, Y v X, Y).
deletef X, Y v Z, Y v Zl):-
delete! X, Z, Zl). delete! x, Y v z, Yl v z)
delete! X, Y, YD.
% ini P, E] -
in! X, X).
in! X, Y):-
delete! X, Y, _).
, , :
[ clause! Cl), delete! P, Cl, CA),
clause! C2), delete! - P, C2, CB) ] >
[ assertz(clause! CA v CB))).
If. Prolog
, . , 23,10, , , :
done(Cl, 2, )
.
, 23.10, , . , , . ,
a v b v -
, . . , :
a v v a
a v b.
, . , , 23.11. translate(Formula}
Cl, C2 .. , .
|
|
|
clause I CD. clause! C2).
23.11. ( )
* ... '"
s- (100, fy, ~). %
:- (110, xfy, &), %
:- (120, xfy, v).
:- (130, xfy, ->). %
% translate) Formula): - % % clausel )
translate! FIG;:- h
I, %
translate(F), translate(G).
translate(Formula):-
transforml Formula, NewFormula), % ,
Formula
!, %
translate(NewForraula).
translate! Formula):- %
assert(clause(Formula)).
% ;
23.
* trans form! Formula]., FormulaZ)
% Formula2 Formulal,
transform* -1-), X).
transform! X => Y, -X v Y).
transform! - (X s YJ, ~X v -Y}.
transform< ~ (X v Y), -X £ -Y).
transform! X S Y v Z, [X v ZJ s IY v Z))
transform! X v Y S Z, [X v Y] fi (X v Z)).
transform! X v y, XI V Y):-transform! X, XI).
| - |
transform! X v Y, X v Yl):-transform! Y, Yl).
| X, - XI) x, XI), |
transform! -transform!
*
%
% % %
*
% %
, , run. , , . , , :?- translate! -((a=>b) S (b=>c)=>U=>O) >, run.
"Contradiction found" ( ), , .
. . Prolog Prolog Prolog.
Prolog, , .
. , . .
- , . , . .
, , , , " ". , , Prolog, , , .
|
|
|
II. Prolog
, , .
:
, ;
;
- :
, , ;
;
, , , ;
, ;
, ;
, ;
, .
