Data.Logic.ATP.FOL

class IsFirstOrder formula

Semantics

data Interp function predicate d

holds

holdsQuantified

holdsAtom

termval

Free Variables

var

fv

fva

fvt

generalize

Substitution

subst

substq

asubst

tsubst

lsubst

bool_interp

mod_interp

Concrete instances of formula types for use in unit tests.

type ApFormula

type EqFormula

Tests

testFOL