Monotonic-Solver

一个设计用于与Rust枚举表达式易于使用的单调求解器

这可以用来

• 研究人工智能常识建模
• 在学习逻辑和语言时测试推理规则
• 生成故事情节
• 搜索和提取数据

用于Avalog，一个具有Prolog-like语法的Avatar逻辑的实验性实现。

博客文章

• 2017-07-25 新的自动单调定理证明库

该库设计的优势在于原型设计的易用性。几个小时之内，人们可以测试建模常识的新想法。

以下是程序输出示例（来自"examples/drama.rs"）

Bob murdered Alice with a gun
Bob shot Alice with a gun
Bob pulled the trigger of the gun
Bob aimed the gun at Alice

这是一个生成戏剧故事情节的程序。求解器从结局开始，反向工作到开始。

• 开始: "Bob用枪杀死了Alice"
• 目标: "Bob把枪对准了Alice"。

您可以逐个步骤地跟踪推理，以自然语言或代码的形式打印出来。

在用这个故事情节写作时，您可能会这样做

Bob picked up the gun and aimed it Alice.
"I hate you!" he cried.
"Wait, I can explain..." Alice raised her hands.
A loud bang.
Bob realized in the same moment what he did.
Something he never would believe if anyone had told him as a child.
He was now a murderer.

这个特定的程序通过利用单调逻辑来向后推理时间。这有助于避免可能世界的爆炸性组合。

技术上，这个求解器在多个矛盾事实导致相同目标时也可以使用。当求解器在找到解决方案后减少证明时，不导致目标的历史将被删除。

示例

以下是"examples/groceries.rs"的完整源代码，该代码确定一个人将从可用的食物和口味偏好中购买哪些水果。

extern crate monotonic_solver;

use monotonic_solver::{search, Solver};

use Expr::*;
use Fruit::*;
use Taste::*;
use Person::*;

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum Person {
    Hannah,
    Peter,
    Clara,
}

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum Taste {
    Sweet,
    Sour,
    Bitter,
    NonSour,
}

impl Taste {
    fn likes(&self, fruit: Fruit) -> bool {
        *self == Sweet && fruit.is_sweet() ||
        *self == Sour && fruit.is_sour() ||
        *self == Bitter && fruit.is_bitter() ||
        *self == NonSour && !fruit.is_sour()
    }
}

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum Fruit {
    Apple,
    Grape,
    Lemon,
    Orange,
}

impl Fruit {
    fn is_sweet(&self) -> bool {
        match *self {Orange | Apple => true, Grape | Lemon => false}
    }

    fn is_sour(&self) -> bool {
        match *self {Lemon | Orange => true, Apple | Grape => false}
    }

    fn is_bitter(&self) -> bool {
        match *self {Grape | Lemon => true, Apple | Orange => false}
    }
}

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum Expr {
    ForSale(Fruit),
    Preference(Person, Taste, Taste),
    Buy(Person, Fruit),
}

fn infer(solver: Solver<Expr>, story: &[Expr]) -> Option<Expr> {
    for expr in story {
        if let &Preference(x, taste1, taste2) = expr {
            for expr2 in story {
                if let &ForSale(y) = expr2 {
                    // Both tastes must be satisfied for the fruit.
                    if taste1.likes(y) && taste2.likes(y) {
                        let new_expr = Buy(x, y);
                        if solver.can_add(&new_expr) {return Some(new_expr)};
                    }
                }
            }
        }
    }
    None
}

fn main() {
    let start = vec![
        ForSale(Orange),
        ForSale(Grape),
        ForSale(Apple),
        ForSale(Lemon),
        Preference(Hannah, Sour, Bitter),
        Preference(Peter, Sour, Sweet),
        Preference(Peter, NonSour, Bitter),
        Preference(Clara, NonSour, Sweet),
    ];
    let order_constraints = vec![
        // Peter likes grape better than orange.
        (Buy(Peter, Grape), Buy(Peter, Orange)),
    ];

    // Look up what this person will buy.
    let person = Peter;

    let (res, _) = search(
        &start,
        |expr| if let &Buy(x, y) = expr {if x == person {Some(y)} else {None}} else {None},
        Some(1000), // max proof size.
        &[],
        &order_constraints,
        infer,
    );
    println!("{:?} will buy:", person);
    for r in res {
        println!("- {:?}", r);
    }
}

当您运行此程序时，它将输出

Peter will buy:
- Grape
- Orange

这是彼得会买的东西。

请注意以下类型的约束

• 人们更喜欢某些水果而不是其他水果
• 一种水果可以提供多种口味体验
• 必须满足所有口味体验，人们才会购买水果
• 并非所有种类的水果都始终可用
• 人们的口味是口味体验的组合
• 人们可能会随着时间的推移改变偏好

当你开始编码一个新的想法时，你可能只对求解器应该做什么有一个模糊的了解。实验吧！

设计

单调求解器是一种自动定理证明器，它通过仅向前搜索来找到证明。单词“单调”意味着新增的事实不会取消先前添加事实的真值。

这个定理证明器是为了在用Rust枚举描述的AST（抽象语法树）上工作而设计的。API是低级别的，以便通过利用HashSet缓存推断事实和过滤来精确控制性能。

• solve_and_reduce最常使用，因为它首先找到证明，然后删除所有推断但无关的事实。
• solve用于展示事实的穷举搜索，例如用于调试。

API能够在不知道任何显式规则的情况下简化证明，因为它在修改过滤器后通过反事实推理。在找到解决方案后，它逐个测试每个事实，通过重新求解问题，从最新添加的事实开始，逐渐移动到开始，以解决隐含的依赖关系。新解决方案中的所有步骤都必须存在于旧解决方案中。由于这可能会发生多次，因此利用缓存非常重要。

每个事实只能添加一次到解决方案中。因此，它不是一个很好的算法，用于长链事件。更适用的领域是建模短期活动的常识。

这是推荐使用这个库的方法

1. 为受限推理领域建模常识
2. 将求解器和约束包装在可理解的编程接口中

目的是使用少量的事实来推断少量额外的事实。在许多应用中，这些额外的事实可能是关键的，因为它们可能对用户来说如此明显，以至于甚至没有被提及。

它还可以在需要序列思考时提高生产力。与计算机相比，人脑在这方面并不擅长这种推理。

挑战是编码使计算机成为一个高效推理器的规则。这就是为什么这个库侧重于以对Rust程序员熟悉的方式提高易用性，以便可以通过短迭代周期测试和比较多个设计。

用法

此库支持两种模式：求解和搜索。

• 在求解模式下，你指定一个目标，求解器尝试找到证明。
• 在搜索模式下，你指定一个模式并提取一些数据。

求解器需要以下5件事

1. 一组起始事实。
2. 一组目标事实。
3. 一组过滤事实。
4. 一组顺序约束。
5. 指向推理算法的函数指针。

起始事实是触发通过规则进行搜索的初始条件。

目标事实决定了何时终止搜索。

过滤事实阻止添加到解决方案中。这可以在算法做出错误假设时用作反馈。

顺序约束用于事实表示事件时。它是一系列形式为(A, B)的元组列表，它控制事件的顺序。事件B临时添加到内部过滤器中，直到事件A发生。

搜索需要以下6件事（与求解器类似，但没有目标）

1. 一组起始事实。
2. 一个匹配模式以提取数据。
3. 一个证明的最大大小以避免内存耗尽。
4. 一组过滤事实。
5. 一组顺序约束。
6. 指向推理算法的函数指针。

通常在这种情况下设置推理算法

fn infer(solver: Solver<Expr>, story: &[Expr]) -> Option<Expr> {
    let places = &[
        University, CoffeeBar
    ];

    for expr in story {
        if let &HadChild {father, mother, ..} = expr {
            let new_expr = Married {man: father, woman: mother};
            if solver.can_add(&new_expr) {return Some(new_expr);}
        }

        if let &Married {man, woman} = expr {
            let new_expr = FellInLove {man, woman};
            if solver.can_add(&new_expr) {return Some(new_expr);}
        }

        ...
    }
    None
}

solver.can_add调用检查该事实是否已被推断。通常还会创建列表以进行迭代，并与其缓存结合使用，以提高查找性能。