[−][src]Struct razor_fol::syntax::Theory

pub struct Theory {
    pub formulae: Vec<Formula>,
}

Is a first-order theory, containing a set of first-order formulae.

Fields

formulae: Vec<Formula>

Is the list of first-order formulae in this theory.

Methods

impl Theory[src]

pub fn gnf(&self) -> Theory[src]

Transforms the given theory to a geometric theory, where all formulae are in Geometric Normal Form (GNF).

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

Example:


let theory: Theory = r#"
    not P(x) or Q(x);
    Q(x) -> exists y. P(x, y);
"#.parse().unwrap();
assert_eq!(r#"P(x) → Q(x)
Q(x) → P(x, sk#0(x))"#, theory.gnf().to_string());

Trait Implementations

impl Display for Theory[src]

impl From<Vec<Formula>> for Theory[src]

impl FromStr for Theory[src]

type Err = Error

The associated error which can be returned from parsing.

Auto Trait Implementations

impl RefUnwindSafe for Theory

impl Send for Theory

impl Sync for Theory

impl Unpin for Theory

impl UnwindSafe for Theory

Blanket Implementations

impl<T> Any for T where
    T: 'static + ?Sized, [src]

impl<T> Borrow<T> for T where
    T: ?Sized, [src]

impl<T> BorrowMut<T> for T where
    T: ?Sized, [src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, [src]

impl<T> ToString for T where
    T: Display + ?Sized, [src]

impl<T, U> TryFrom<U> for T where
    U: Into<T>, [src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, [src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.