命题表求解器

使用命题表方法编写的一个小型命题公式可满足性求解器，使用 Rust 编程语言实现！

见 http://www.dis.uniroma1.it/liberato/planning/tableau/tableau.html.

命题公式的语法

求解器的输入必须是良好形式的命题公式。

它可以由以下 BNF 语法描述

<formula>   ::= <propositional-variable>
            |   ( - <formula> )             # negation
            |   ( <formula> ^ <formula>  )  # conjunction
            |   ( <formula> | <formula>  )  # disjunction
            |   ( <formula> -> <formula>  ) # implication
            |   ( <formula> <-> <formula> ) # bi-implication

空白字符被删除并忽略，一个 <propositional-variable> 可以是任何以字母字符开头的数字字母字符序列 [a-zA-Z][a-zA-Z0-9]*。大小写敏感，aaa 与 AAA 是不同的命题变量。

通过 Cargo 运行

模式

CLI 支持对给定命题公式的 satisfiability 模式和 validity 模式进行检查。

使用 -m 模式开关

1. 有效性模式：-m v.
2. 可满足性模式（默认）：-m s.

输入

有两种方式提供命题公式，使用 - 开关方法具有优先级

$ cargo run -c "(a^b)"

$ cat input.txt > cargo run