Enum resolution_prover::Proposition

pub enum Proposition {
    Or(Box<Proposition>, Box<Proposition>),
    And(Box<Proposition>, Box<Proposition>),
    Implies(Box<Proposition>, Box<Proposition>),
    Iff(Box<Proposition>, Box<Proposition>),
    Not(Box<Proposition>),
    Term(String),
}

A statement in propositional logic.

For example, p /\ (~q) would be representated in the following way.

let p = resolution_prover::term("p".to_string());
let q = resolution_prover::term("q".to_string());

let not_q = resolution_prover::not(q);

let p_and_not_q = resolution_prover::and(p, not_q);

Variants

Or(Box<Proposition>, Box<Proposition>)And(Box<Proposition>, Box<Proposition>)Implies(Box<Proposition>, Box<Proposition>)Iff(Box<Proposition>, Box<Proposition>)Not(Box<Proposition>)Term(String)

Trait Implementations

impl Debug for Proposition

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

Formats the value using the given formatter.

impl PartialEq for Proposition

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

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

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

This method tests for !=.

impl Clone for Proposition

fn clone(&self) -> Proposition

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Display for Proposition

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

Displays the proposition using cominations of ascii characters to represent the propositional logic operations.

let hello = resolution_prover::Proposition::Term("hello".to_string());
let hi = resolution_prover::Proposition::Term("hi".to_string());

let not_hi = resolution_prover::not(hi);

let hello_and_not_hi = resolution_prover::and(hello, not_hi);

let expected = String::from("hello /\\ ~(hi)");

assert_eq!(format!("{}", hello_and_not_hi), expected);