[Prolog] First order logic formule

[Marc]

Ik probeer een manier te vinden om de volgende first order logica formule naar Prolog te vertalen:

code:

(p(0) or p(1)) and not (p(0) and p(1))

Dit betekent dat ik de volgende output zou moeten krijgen:

code:

?- p(0)
Yes.
?- p(1)
Yes.
?- p(0),p(1).
No.

Ik heb eerst de logica herschreven:

code:

(p(0) or p(1)) and not (p(0) and p(1)) <=>
(not p(0) -> p(1)) and (p(0) -> not p(1)) <=>
p(0) <-> not p(1)

Gebruikmakend van "Clarks completion" (dit is een semantics die stelt dat elke definitional theory in een logisch programma gezet kan worden door gebruik te maken van de if-halves), kan ik de volgende Prolog code verkrijgen:

Prolog:

p(0) :- not p(1).

Helaas is deze theory alleen correct (er zal geen foute informatie afgeleid worden), maar niet compleet (ik kan bijvoorbeeld p(1) niet afleiden). Dit is een consequentie van Clarks completion.

Weet iemand of er een betere manier is die een equivalent logisch programma oplevert?

[Infinitive]

Ik begrijp je vraag waarschijnlijk verkeerd, maar dat je p(1) niet kan afleiden is omdat je er geen passende afleidingsregel voor hebt. Ik zou dan eigenlijk een regels verwachten zoals:

Prolog:

p(0) :- not  p(1)
p(1) :- not  p(0)

(een dergelijk cyclische definitie is neem ik aan geen probleem voor prolog...)

Jouw formule staat niet toe dat je individueel p(0) of p(1) kan afleiden zonder extra aannamen. Dit kan natuurlijk alleen wanneer 'not p(0)' of 'not p(1)' geldt!

[ Voor 7% gewijzigd door Infinitive op 29-09-2012 21:21 ]

[Wolfboy]

Het is toch simpelweg een xor?

Dus waarom niet iets als:

code:

p(0) xor p(1)

[Soultaker]

Marc schreef op vrijdag 28 september 2012 @ 15:33:
Dit betekent dat ik de volgende output zou moeten krijgen:

code:

?- p(0)
Yes.
?- p(1)
Yes.
?- p(0),p(1).
No.

Dit gaat nooit gebeuren, aangezien p(0) noch p(1) variabelen bindt, dus als p(0) succeed en p(1) succeed, dan zal p(0), p(1) ook altijd succeeden, ongeacht de definitie van p(0) en p(1) (aangenomen dat je je tot het "logische" deel van Prolog beperkt ).

Infinitive schreef op zaterdag 29 september 2012 @ 21:21:

Prolog:

p(0) :- not  p(1)
p(1) :- not  p(0)

(een dergelijk cyclische definitie is neem ik aan geen probleem voor prolog...)

Je kunt dit wel schrijven (met iets andere syntax) maar dan krijg je een oneindige lus. Immers moet je om p(0) af te leiden proberen p(1) af te leiden, en om p(1) af te leiden moet je proberen p(0) af te leiden, en zo voorts.

De formule uit de TS kun je wel schrijven als:

Prolog:

p(0), \+ p(1);
p(1), \+ p(0).

Wolfboy schreef op zaterdag 29 september 2012 @ 21:59:
Het is toch simpelweg een xor?

Dus waarom niet iets als:

code:

p(0) xor p(1)

Leuk, maar een predicate is geen functie.

[ Voor 16% gewijzigd door Soultaker op 29-09-2012 22:36 ]

[Marc]

Soultaker schreef op zaterdag 29 september 2012 @ 22:34:
[...]

De formule uit de TS kun je wel schrijven als:

Prolog:

p(0), \+ p(1);
p(1), \+ p(0).

Dat klopt, alleen is deze formula nutteloos omdat je hem niet direct in een Prolog file kunt zetten. Het lijkt er dus op dat dit in het algemeen niet mogelijk is, bedankt voor de reacties.