GraphProver

• Index

Contents

• Methods
• Metamethods

Classes

• graph
• wff

Class wff

Well-formed, propositional formulas.

Methods

wff:is_and ()	Tests whether formula is a conjunction.
wff:is_atom ()	Tests whether formula is an atom.
wff:is_iff ()	Tests whether formula is a bi-implication.
wff:is_immediate_sub (other)	Tests whether formula is an immediate formula of another.
wff:is_imp ()	Tests whether formula is an implication.
wff:is_not ()	Tests whether formula is a negation.
wff:is_or ()	Tests whether formula is a disjunction.
wff:is_proper_sub (other)	Tests whether formula is a proper formula of another
wff:new (sym)	Creates a new atomic formula
wff:parse (s)	Parses formula string.
wff:sym ()	Gets formula symbol.
wff:tag ()	Gets formula tag.
wff:unpack ()	Gets immediate subformulas of formula.

Metamethods

wff:__eq (other)

Tests whether formula is syntactically equal to another.

Methods

wff:is_and ()

Tests whether formula is a conjunction.

Returns:

true if formula is a conjunction

Or

false otherwise

wff:is_atom ()

Tests whether formula is an atom.

Returns:

true if formula is an atom

Or

false otherwise

wff:is_iff ()

Tests whether formula is a bi-implication.

Returns:

true if formula is a bi-implication

Or

false otherwise

wff:is_immediate_sub (other)

Tests whether formula is an immediate formula of another.

Parameters:

• other wff the other formula

Returns:

true if successful

Or

false otherwise

wff:is_imp ()

Tests whether formula is an implication.

Returns:

true if formula is a implication

Or

false otherwise

wff:is_not ()

Tests whether formula is a negation.

Returns:

true if formula is a negation

Or

false otherwise

wff:is_or ()

Tests whether formula is a disjunction.

Returns:

true if formula is a disjunction

Or

false otherwise

wff:is_proper_sub (other)

Tests whether formula is a proper formula of another

Parameters:

• other wff the other formula

Returns:

true if successful

Or

false otherwise

wff:new (sym)

Creates a new atomic formula

Parameters:

• sym string formula symbol

Returns:

the resulting atomic formula

Or

nil plus error message

wff:parse (s)

Parses formula string.

Parameters:

• s string formula string

Returns:

the resulting formula

Or

nil plus error message

wff:sym ()

Gets formula symbol.

Returns:

the formula symbol

wff:tag ()

Gets formula tag.

Returns:

the formula tag ('atom', 'not', 'and', 'or', 'imp', or, 'iff')

wff:unpack ()

Gets immediate subformulas of formula.

Returns:

wff,... all immediate subformulas of formula

Metamethods

wff:__eq (other)

Tests whether formula is syntactically equal to another.

Parameters:

• other wff the other formula

Returns:

true if successful

Or

false otherwise