Declarative programming: ข้อเท็จจริง กฎ และเป้าหมาย

询问谁可以借用相机

• A media club keeps facts about its members and completed training. It wants to ask who can borrow a camera without writing a new loop for every question.
• 声明式编程描述事实、规则和目标。逻辑引擎搜索使目标为真的值。程序员仍然需要编写正确的规则；引擎不会读取思想或俱乐部公告板。

事实陈述已知内容

• 事实是知识库中的断言。在 member(aya). 中，谓词 member 将一个人与俱乐部会员资格联系起来。 trained(aya, camera). 将人与设备联系起来。
• This lesson uses Prolog-style notation: lowercase names are constants or predicates; uppercase names are variables. A full stop ends each fact or rule.

member(aya).
member(ben).
member(chen).
trained(aya, camera).
trained(chen, camera).
trained(ben, audio).

规则组合条件

• 规则说明何时结论成立。将 :- 读作“如果”，逗号表示AND：一个人可以借用相机，前提是他是会员 并且 拥有相机培训。
• Person 在所有三个地方命名同一个变量。引擎必须找到一个同时满足两个条件的值，而不是一个会员和一个不同的受训人员。

can_borrow(Person, camera) :- member(Person), trained(Person, camera).

目标提出问题

• The goal ?- can_borrow(aya, camera). asks for a yes/no result. The engine matches the rule and checks member(aya) and trained(aya, camera): both facts exist, so the goal succeeds.
• The goal ?- can_borrow(Person, camera). asks for bindings of the variable. With this knowledge base, the answers are Person = aya and Person = chen. These are goals to reason about; the displayed blocks are notation, not a runnable playground.

工作示例：追踪失败的候选人

การจับคู่จะแบ่งปันค่าผ่านกฎ

• Unification matches terms while consistently binding variables. Matching trained(Person, camera) with trained(chen, camera) binds Person to chen; matching it with trained(ben, audio) fails because the equipment differs.
• เป้าหมายที่ล้มเหลวหมายความว่าไม่สามารถพิสูจน์ได้จากข้อเท็จจริงและกฎเหล่านี้ มันไม่ได้พิสูจน์ว่า Ben ไม่เคยใช้กล้องในชีวิตจริงเลย;ฐานความรู้อาจมีเพียงส่วนที่ไม่สมบูรณ์เท่านั้น

ตัวอย่างแสดงวิธีทำ: เขียนกฎใหม่

can_help(Mentor, Learner) :- trained(Mentor, camera), member(Learner).

คะแนนที่หลุดหายไป

จากข้อกำหนดไปสู่การพิสูจน์