Module cop::fof

source ·
Expand description

First-order formulas and various normal forms.

Structs

  • Forall
    Universal quantifier.
  • SkolemState
    The state of Skolemisation at a given position in a formula.

Enums

  • Cnf
    Conjunctive normal form of literals L, preserving parentheses.
  • Dnf
    Disjunction of literals that preserves parentheses.
  • Fof
    Full first-order formula over atoms A and variables V.
  • FofAtom
    Atoms occurring in a FOF, containing predicates P, constants C, and variables V.
  • Nnf
    Negation-normal form of literals L, variables V, and quantifiers V.
  • Op
    Binary operation.
  • OpA
    Associative binary operation.
  • Quantifier
    Quantifier.

Functions

  • join
    Given x and y1 o … o yn, return x if n = 0, else x o y1 o … o yn.