logic

package logic
First-order logic data structure and algorithm.

Concerns

  • logic: First-order logic data structure and algorithm.
    • lexpr: Logical expression.
    • logic: First-order logic data structure and algorithm.

logic::lexpr

module lexpr

Logical expression.

This module provides a simple data structure for first order logic. Basic logical operators and algorithms are provided.

var a = new LVar("a")
var b = new LVar("b")
var c = new LVar("c")

assert a.to_s == "a"
assert (a|b).to_s == "(a | b)"
assert (~(a|b)).to_s == "~(a | b)"

Compute a negative normal form:

var ex = a | (b & c)
var nex = ~ex
assert ex.nnf.to_s == "(a | (b & c))"
assert nex.nnf.to_s == "(~a & (~b | ~c))"

Compute a conjunctive normal form:

assert ex.cnf.simplify.to_s == "(a|b) & (a|c)"
assert nex.cnf.simplify.to_s == "(~a) & (~b|~c)"
Introduces
  • LExpr: A logical expression
  • CNF: A conjunctive normal form of a logical expression.
  • LAnd: A logical conjunction operation
  • LOr: A logical disjunction operation
  • LNot: A logical negation operation
  • LTrue: The class of the singleton ltrue
  • LFalse: The class of the singleton lfalse
  • LVar: A variable of a logical expression.
Redefines
  • Sys: The main class of the program.