قرار البديهية

Question

أحاول أن أفهم كيف يعمل حل Axiom في Prolog.

لنفترض أنني أحدد العمليتين الأساسيتين على الأرقام الطبيعية:

• S (المصطلح) (يقف للخلف) و

• إضافة (مصطلح ، آخر).

يتم إعطاء الدلالي من ADD بواسطة

• إضافة (0 ، x1) -> x1

• إضافة (x1 ، 0) -> x1

• إضافة (s (x1) ، y1) -> s (إضافة (x1 ، y1))

ثم ، أود حل المعادلة

إضافة (x ، إضافة (y ، z)) = s (0)

أتصور أن استراتيجية واحدة يمكن أن تكون

• اختبار إذا كان الجانب الأيمن (RHS) للمعادلة يساوي الجانب الأيسر (LHS)

• إذا لم تكن ترى ما إذا كان يمكن العثور على حل من خلال البحث عن أكثر الأحاديات

• إذا لم يكن الأمر كذلك ، فحاول العثور على بديهية يمكن استخدامها في هذه المعادلة. يمكن أن تكون الإستراتيجية للقيام بهذه المهمة (لكل بديهية): حاول حل RHS للمعادلة تساوي RHs من البديهية. إذا كان هناك حل ، فحاول حل LHS للمعادلة يساوي LHS من البديهية. إذا نجحت ، فقد وجدنا البديهية الصحيح.

• في نهاية المطاف ، إذا لم يكن هناك حل و LHS و RHs للمعادلة هما نفس العملية (أي نفس التوقيع ولكن ليس نفس المعاملات) ، فطبق الخوارزمية على كل معامل ويتم العثور على حل إذا تم العثور على حل لكل معامل.

أعتقد أن هذه الخوارزمية (البسيطة) قد تعمل. ومع ذلك ، أود أن أعرف ما إذا كان لدى أي شخص خبرة في حل هذا النوع من المشكلات؟ هل يعرف أي شخص أين يمكنني العثور على بعض الوثائق حول خوارزمية أفضل؟

شكرا مقدما

Answer 1

ما تبحث عنه يسمى تضييق. يتم تنفيذه في بعض اللغات الوظيفية مثل كاري, ، ولكن ليس في مقدمة نفسها.

Answer 2

برنامج Prolog هو مجموعة من المتنبئين.

المسند هو مجموعة من الجمل.

بند له النموذج

Head :- Body.

المعنى "Head صحيح إذا Body صحيح".

هناك شكل شرط مختصر

Head.

وهو ما يعني نفس الشيء

Head :- true.

أين true هو مصمم صحيح دائما.

العودة إلى Body جزء من جملة ، Body هو الهدف الذي يمكن أن يأخذ أحد الأشكال التالية (A, B, ، و C تشير إلى الأهداف التعسفية):

Atom            % This is true if Atom is true (see below).
A, B            % This is true if A is true and B is true.
(A ; B)         % This is true if A is true or B is true.
\+ A            % This is true if A is not true.
(A -> B ; C)    % If A is true then B must be true, else C must be true.

هناك بعض القواعد الخاصة في Prolog فيما يتعلق بترتيب التقييم (من اليسار إلى اليمين) و "التخفيضات" (التي تقلب شجرة البحث) ، ولكن هذه تفاصيل رائعة تتجاوز نطاق هذا البرنامج التعليمي الموجز.

الآن ، لتقرير ما إذا كان Atom صحيح، Atom يمكن أن يكون أحد الأشكال التالية (X و Y تشير إلى المصطلحات التعسفية):

true                % or some other builtin with given truth rules.
X = Y               % True if X and Y are successfully unified.
p(X, Y, ...)        % True if p(X, Y, ...) matches the head of some clause
                    % and the Body is true.

المصطلح هو ، في الأساس ، أي قطعة من بناء الجملة.

الشيء الرئيسي الذي يجب اكتشافه هنا هو أن Prolog ليس لديه وظائف! حيث يمكنك تحديد وظيفة في لغة وظيفية add(X, Y) الذي يقيم إلى مجموع X و Y, ، في المقدمة ، تحدد مسندًا رأسه add(X, Y, Z) الذي ، إذا نجحت ، يوحد Z مع المصطلح الذي يشير إلى مجموع X و Y.

بالنظر إلى كل ذلك ، يمكننا تحديد قواعدك في Prolog على النحو التالي:

add(0, Y, Y).                        % 0 + Y = Y.
add(Y, 0, Y).                        % Y + 0 = Y.
add(s(X), Y, s(Z)) :- add(X, Y, Z).  % s(X) + Y = s(X + Y).

أين أستخدم 0 للدلالة على الصفر (!) و s(X) للدلالة على خليفة X.

النظر في التقييم add(s(s(0)), s(0), Z):

add(s(s(0)), s(0), Z)                 % Only the third head for add matches, so...
---> Z = s(Z0), add(s(0), s(0), Z0).

add(s(0), s(0), Z0)                   % Only the third head for add matches, so...
---> Z0 = s(Z1), add(0, s(0), Z1).

add(0, s(0), Z1)                      % Only the first head for add matches, so...
---> Z1 = s(0).

وضع كل تلك التوحيد ل Z معا ، لدينا Z = s(s(s(0))).

الآن ، قد تسأل "ماذا يحدث إذا كان أكثر من رأس واحد يتطابق في فقرة" أو "ماذا يحدث إذا فشل مسار التقييم؟" ، والتي تكون الإجابات "غير المحددة" ، "التراجع" ، وبشكل عام ، اقرأ أ كتاب مقدمة!

أتمنى أن يساعدك هذا.

Answer 3

"تمثيل المعرفة والتفكير" من تأليف Brachmann و Levesque يقدم مقدمة جيدة إلى حد ما لكيفية عمل هذه الأشياء.