linear_solver

一个为方便与Rust枚举一起使用而设计的线性求解器。

这是一个用于自动定理证明的库。

线性求解意味着某些事实可以被其他事实替换。这种技术也可以用来使定理证明更有效。

如果您正在寻找不删除事实的求解器，
请参阅 monotonic_solver

注意！此求解器不支持多历史记录。
它假定当事实被简化时，它们证明的事实集合与简化后的事实集合相同。

线性求解器可用于

• 在线性逻辑中证明某些事物
• 更有效地在经典逻辑中证明某些事物
• 证明某些关于资源“消耗”位置的事物
• 约束求解
• 实现某些约束求解编程语言

本项目受到了 CHR (Constraint Handling Rules) 的极大启发

示例：行走

/*

In this example, we reduce a walk (left, right, up, down):

    l, l, u, l, r, d, d, r
    ----------------------
    l, u

*/

extern crate linear_solver;

use linear_solver::{solve_minimum, Inference};
use linear_solver::Inference::*;

use std::collections::HashSet;

use self::Expr::*;

#[derive(Clone, PartialEq, Eq, Debug, Hash)]
pub enum Expr {
    Left,
    Right,
    Up,
    Down,
}

pub fn infer(cache: &HashSet<Expr>, _facts: &[Expr]) -> Option<Inference<Expr>> {
    // Put simplification rules first to find simplest set of facts.
    if cache.contains(&Left) && cache.contains(&Right) {
        return Some(ManyTrue {from: vec![Left, Right]});
    }
    if cache.contains(&Up) && cache.contains(&Down) {
        return Some(ManyTrue {from: vec![Up, Down]});
    }
    None
}

fn main() {
    let start = vec![
        Left,
        Left,
        Up,
        Left,
        Right,
        Down,
        Down,
        Right,
    ];

    let res = solve_minimum(start, infer);
    for i in 0..res.len() {
        println!("{:?}", res[i]);
    }
}

示例：小于等于

/*

In this example, we prove the following:

    X <= Y
    Y <= Z
    Z <= X
    ------
    Y = Z
    Y = X

*/

extern crate linear_solver;

use linear_solver::{solve_minimum, Inference};
use linear_solver::Inference::*;

use std::collections::HashSet;

use self::Expr::*;

#[derive(Clone, PartialEq, Eq, Debug, Hash)]
pub enum Expr {
    Var(&'static str),
    Le(Box<Expr>, Box<Expr>),
    Eq(Box<Expr>, Box<Expr>),
}

pub fn infer(cache: &HashSet<Expr>, facts: &[Expr]) -> Option<Inference<Expr>> {
    // Put simplification rules first to find simplest set of facts.
    for ea in facts {
        if let Le(ref a, ref b) = *ea {
            if a == b {
                // (X <= X) <=> true
                return Some(OneTrue {from: ea.clone()});
            }

            for eb in facts {
                if let Le(ref c, ref d) = *eb {
                    if a == d && b == c {
                        // (X <= Y) ∧ (Y <= X) <=> (X = Y)
                        return Some(Inference::replace(
                            vec![ea.clone(), eb.clone()],
                            Eq(a.clone(), b.clone()),
                            cache
                        ))
                    }
                }
            }
        }

        if let Eq(ref a, ref b) = *ea {
            for eb in facts {
                if let Le(ref c, ref d) = *eb {
                    if c == b {
                        // (X = Y) ∧ (Y <= Z) <=> (X = Y) ∧ (X <= Z)
                        return Some(Inference::replace_one(
                            eb.clone(),
                            Le(a.clone(), d.clone()),
                            cache
                        ));
                    } else if d == b {
                        // (X = Y) ∧ (Z <= Y) <=> (X = Y) ∧ (Z <= X)
                        return Some(Inference::replace_one(
                            eb.clone(),
                            Le(c.clone(), a.clone()),
                            cache
                        ));
                    }
                }

                if let Eq(ref c, ref d) = *eb {
                    if b == c {
                        // (X = Y) ∧ (Y = Z) <=> (X = Y) ∧ (X = Z)
                        return Some(Inference::replace_one(
                            eb.clone(),
                            Eq(a.clone(), d.clone()),
                            cache
                        ));
                    }
                }
            }
        }
    }

    // Put propagation rules last to find simplest set of facts.
    for ea in facts {
        if let Le(ref a, ref b) = *ea {
            for eb in facts {
                if let Le(ref c, ref d) = *eb {
                    if b == c {
                        // (X <= Y) ∧ (Y <= Z) => (X <= Z)
                        let new_expr = Le(a.clone(), d.clone());
                        if !cache.contains(&new_expr) {return Some(Propagate(new_expr))};
                    }
                }
            }
        }
    }
    None
}

pub fn var(name: &'static str) -> Box<Expr> {Box::new(Var(name))}

fn main() {
    let start = vec![
        Le(var("X"), var("Y")), // X <= Y
        Le(var("Y"), var("Z")), // Y <= Z
        Le(var("Z"), var("X")), // Z <= X
    ];

    let res = solve_minimum(start, infer);
    for i in 0..res.len() {
        println!("{:?}", res[i]);
    }
}

线性逻辑

当某些事实被简化时，例如

X, Y <=> Z

您需要两个新的 X 和 Y 副本来推断另一个 Z。这是因为求解器没有删除所有副本。

在用线性求解器进行经典定理证明时，通常需要检查输入中每个事实都是唯一的，并且在添加新事实之前检查 cache。这确保求解器不会添加重复的事实。

然而，在进行线性定理证明时，可以为每个 X 和 Y 生成重复的事实 Z。

目标的意义

由于线性求解器可以同时引入和删除事实，这意味着在证明目标的意义上没有终止，因为目标可以在以后被删除。

相反，当一个目标属于同一个“循环”时，它被认为是已证明的。这是使用具有停止扩展的规则的确定性求解器使用的事实集合的重复列表。

循环中最小的事实集被视为隐含目标，因为循环中所有其他事实都可以从这个事实集中推断出来。

请注意，循环中的最小事实集与最小公理集不同。最小公理集是一组事实，用更少的事实证明了最小事实集。换句话说，最小公理集开始于循环之外。当它移动到循环内部时，它与某些最小事实集相同。

最小事实集和最小公理集都可以用来识别两组事实之间的等价性。

false和true的直觉

false的直觉可以理解为

• 一些可以从其中证明所有事实的事实
• 一些可以将每个矛盾简化的事实
• 包含每个真值都存在矛盾的语言

在包含false的循环中，该语言的最小事实集是false。

true的直觉可以理解为

• 一些可以从其中证明每个初始事实的事实
• 与false矛盾的某些事实

这意味着初始事实隐含着true，并且由于它与false矛盾，如果初始事实中存在矛盾，则它们可以证明false。

因此，如果它的最小事实集不等于false，则从初始事实得出的证明是true。