Enum razor_fol::syntax::Formula

pub enum Formula {
    Top,
    Bottom,
    Atom {
        predicate: Pred,
        terms: Vec<Term>,
    },
    Equals {
        left: Term,
        right: Term,
    },
    Not {
        formula: Box<Formula>,
    },
    And {
        left: Box<Formula>,
        right: Box<Formula>,
    },
    Or {
        left: Box<Formula>,
        right: Box<Formula>,
    },
    Implies {
        left: Box<Formula>,
        right: Box<Formula>,
    },
    Iff {
        left: Box<Formula>,
        right: Box<Formula>,
    },
    Exists {
        variables: Vec<V>,
        formula: Box<Formula>,
    },
    Forall {
        variables: Vec<V>,
        formula: Box<Formula>,
    },
}

Is an abstract syntax tree (AST) for first-order formulae.

Variants

Top

Is logical Top (⊤) or Truth

Bottom

Is logical Bottom (⟘) or Falsehood

Atom

Is an atomic formula, made by applying predicate on a list of terms.

Fields of Atom

predicate: Predterms: Vec<Term>

Equals

Represents an equality between two terms.

Note: Equality is a special type of atomic formula.

Fields of Equals

left: Termright: Term

Not

Makes the negation of the formula that it holds.

Fields of Not

formula: Box<Formula>

And

Makes a conjunction of the left and right formulae that it holds.

Fields of And

left: Box<Formula>right: Box<Formula>

Or

Makes a disjunction of left and right formulae that it holds.

Fields of Or

left: Box<Formula>right: Box<Formula>

Implies

Makes an implication between left and right formulae that it holds.

Fields of Implies

left: Box<Formula>right: Box<Formula>

Iff

Makes a bi-implication between left and right formulae that it holds.

Fields of Iff

left: Box<Formula>right: Box<Formula>

Exists

Makes an existentially quantified formula with the bound variables and the formula that it holds.

Fields of Exists

variables: Vec<V>formula: Box<Formula>

Forall

Makes a universally quantified formula with the bound variables and the formula that it holds.

Fields of Forall

variables: Vec<V>formula: Box<Formula>

Methods

impl Formula

pub fn and(self, formula: Self) -> Self

Returns a conjunction of the receiver and formula.

pub fn or(self, formula: Self) -> Self

Returns a disjunction of the receiver and formula.

pub fn implies(self, formula: Self) -> Self

Returns an implication between the receiver and formula.

pub fn iff(self, formula: Self) -> Self

Returns a bi-implication between the receiver and formula.

pub fn free_vars(&self) -> Vec<&V>

Returns a list of free variable symbols in the receiver formula.

Note: In the list of free variables, each variable symbol appears only once even if it is present at multiple positions of the receiver formula.

Example:

// `x`, `y` and `z` are variable symbols:
let x = V::from("x");
let y = V::from("y");
let z = V::from("z");

// (P(x) ∧ Q(x, f(g(x), y))) ∨ ('c = g(z))
let formula: Formula = "(P(x) & Q(x, f(g(x), y))) |  'c = g(z)".parse().unwrap();
assert_eq!(vec![&x, &y, &z].iter().sorted(), formula.free_vars().iter().sorted());

// ∀ x. P(x, y)
let formula: Formula = "forall x. P(x, y)".parse().unwrap();
// notice that the bound variable `x` is not in the list of free variables of `formula`
assert_eq!(vec![&y], formula.free_vars());

// ∃ x. P(x, y)
let formula: Formula = "exists x. P(x, y)".parse().unwrap();
assert_eq!(vec![&y], formula.free_vars());

impl Formula

pub fn pnf(&self) -> Formula

Returns a Prenex Normal Form (PNF) equivalent to the receiver.

Hint: A PNF is a formula with all quantifiers (existential and universal) and bound variables at the front, followed by a quantifier-free part.

Example:

let formula: Formula = "Q(x, y) → ∃ x, y. P(x, y)".parse().unwrap();
assert_eq!("∃ x`, y`. (Q(x, y) → P(x`, y`))", formula.pnf().to_string());

pub fn snf(&self) -> Formula

Returns a Skolem Normal Form (SNF) equivalent to the receiver.

Hint: An SNF is a PNF with only universal quantifiers (see: https://en.wikipedia.org/wiki/Skolem_normal_form).

Example:

let formula: Formula = "∃ y. P(x, y)".parse().unwrap();
assert_eq!("P(x, sk#0(x))", formula.snf().to_string());

pub fn snf_with(&self, generator: &mut SkolemGenerator) -> Formula

Is similar to Formula::snf but uses an existing SkolemGenerator to avoid collision when generating Skolem function names (including Skolem constants).

Example:

use razor_fol::transform::SkolemGenerator;

let mut generator = SkolemGenerator::from("skolem");
let formula: Formula = "∃ y. P(x, y)".parse().unwrap();
assert_eq!("P(x, skolem0(x))", formula.snf_with(&mut generator).to_string());

pub fn nnf(&self) -> Formula

Returns an Negation Normal Form (NNF) equivalent to the receiver.

Hint: An NNF is a formula where negation is only applied to its atomic (including equations) sub-formulae.

Example:

let formula: Formula = "not (P(x) iff Q(y))".parse().unwrap();
assert_eq!("(P(x) ∧ (¬Q(y))) ∨ ((¬P(x)) ∧ Q(y))", formula.nnf().to_string());

pub fn cnf(&self) -> Formula

Returns a Conjunctive Normal Form (CNF) equivalent to the receiver.

Hint: A CNF is a formula that is a conjunction of zero or more clauses. A clause is a disjunction of atomic formulae (including equations).

Note: All free variables are assumed to be universally quantified.

Example:

let formula: Formula = "P(x) <=> Q(y)".parse().unwrap();
assert_eq!("((¬P(x)) ∨ Q(y)) ∧ ((¬Q(y)) ∨ P(x))", formula.cnf().to_string());

pub fn cnf_with(&self, generator: &mut SkolemGenerator) -> Formula

Is similar to Formula::cnf but uses an existing SkolemGenerator to avoid collision when generating Skolem function names (including Skolem constants).

Note: The CNF transformation includes Skolemization.

Example:

use razor_fol::transform::SkolemGenerator;

let mut generator = SkolemGenerator::from("s%");
let formula: Formula = "exists x. ((forall y. P(y) & Q(x, y))  -> R(x))".parse().unwrap();
assert_eq!("((¬P(\'s%1)) ∨ (¬Q(\'s%0, \'s%1))) ∨ R(\'s%0)",
    formula.cnf_with(&mut generator).to_string());

pub fn dnf(&self) -> Formula

Returns a Disjunctive Normal Form (DNF) equivalent to the receiver.

Hint: A DNF is a formula that is a disjunction of zero or more conjuncts. A conjunct is a conjunction of atomic formulae (including equations).

Note: All of the free variables are assumed to be universally quantified.

Example:

let formula: Formula = "P(x) iff Q(y)".parse().unwrap();
assert_eq!("(((¬P(x)) ∧ (¬Q(y))) ∨ ((¬P(x)) ∧ P(x))) ∨ ((Q(y) ∧ (¬Q(y))) ∨ (Q(y) ∧ P(x)))",
    formula.dnf().to_string());

pub fn dnf_with(&self, generator: &mut SkolemGenerator) -> Formula

Is similar to Formula::dnf but uses an existing SkolemGenerator to avoid collision when generating Skolem function names (including Skolem constants).

Note: The DNF transformation includes Skolemization.

Example:

use razor_fol::transform::SkolemGenerator;

let mut generator = SkolemGenerator::from("s%");
let formula: Formula = "!y. (!x. (P(y, x) | Q(x)) -> Q(y))".parse().unwrap();
assert_eq!("((¬P(y, s%0(y))) ∧ (¬Q(s%0(y)))) ∨ Q(y)",
    formula.dnf_with(&mut generator).to_string());

pub fn simplify(&self) -> Formula

Applies a number of syntactic transformations to simplify the receiver formula.

Example:

let formula: Formula = "not (not P())".parse().unwrap();
assert_eq!("P()", formula.simplify().to_string());

let formula: Formula = "forall x. (P() and true) | (Q(x) or false)".parse().unwrap();
assert_eq!("∀ x. (P() ∨ Q(x))", formula.simplify().to_string());

pub fn gnf(&self) -> Vec<Formula>

Returns a list of formulae in Geometric Normal Form (GNF), equivalent to the receiver.

Hint: For mor information about GNF, see Geometric Logic in Computer Science by Steve Vickers.

Example:

let formula: Formula = "P(x) & (Q(x) | R(x))".parse().unwrap();
let gnf_to_string: Vec<String> = formula.gnf().iter().map(|f| f.to_string()).collect();
assert_eq!(vec!["⊤ → P(x)", "⊤ → (Q(x) ∨ R(x))"], gnf_to_string);

pub fn gnf_with(&self, generator: &mut SkolemGenerator) -> Vec<Formula>

Is similar to Formula::gnf but uses an existing SkolemGenerator to avoid collision when generating Skolem function names (including Skolem constants).

Note: The GNF transformation includes Skolemization.

Example:

use razor_fol::transform::SkolemGenerator;

let mut generator = SkolemGenerator::from("s%");
let formula: Formula = "P(y) -> exists x. P(x) & Q(y)".parse().unwrap();
let gnf_to_string: Vec<String> = formula.gnf().iter().map(|f| f.to_string()).collect();
assert_eq!(vec!["P(y) → P(sk#0(y))", "P(y) → Q(y)"], gnf_to_string);

Trait Implementations

impl Clone for Formula

fn clone(&self) -> Formula

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Formula

fn fmt(&self, f: &mut Formatter) -> Result<(), Error>

Formats the value using the given formatter.

impl Display for Formula

fn fmt(&self, f: &mut Formatter) -> Result<(), Error>

Formats the value using the given formatter.

impl Eq for Formula

impl FromStr for Formula

type Err = Error

The associated error which can be returned from parsing.

fn from_str(s: &str) -> Result<Self, Self::Err>

Parses a string s to return a value of this type.

impl Hash for Formula

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given [Hasher].

impl Ord for Formula

fn cmp(&self, other: &Formula) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

🔬 This is a nightly-only experimental API. (clamp)

Restrict a value to a certain interval.

impl PartialEq<Formula> for Formula

fn eq(&self, other: &Formula) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Formula) -> bool

This method tests for !=.

impl PartialOrd<Formula> for Formula

fn partial_cmp(&self, other: &Formula) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Formula) -> bool

This method tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Formula) -> bool

This method tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Formula) -> bool

This method tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Formula) -> bool

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl StructuralEq for Formula

impl StructuralPartialEq for Formula

impl TermBased for Formula

fn transform(&self, f: &impl Fn(&Term) -> Term) -> Self

Applies a transformation function f on the [Term]s of the receiver.

fn rename_vars(&self, renaming: &impl VariableRenaming) -> Self

Note: Applies a VariableRenaming on the free variables of the formula, keeping the bound variables unchanged.

fn substitute(&self, substitution: &impl Substitution) -> Self

Note: Applies a Substitution on the free variables of the formula, keeping the bound variables unchanged.