Data.Logic.ATP.Prolog

Backchaining procedure for Horn clauses, and toy Prolog implementation.

Documentation

data PrologRule lit

Constructors

Prolog (Set lit) lit

Instances

Eq lit => Eq (PrologRule lit)

Methods

(==) :: PrologRule lit -> PrologRule lit -> Bool

(/=) :: PrologRule lit -> PrologRule lit -> Bool

Ord lit => Ord (PrologRule lit)

Methods

compare :: PrologRule lit -> PrologRule lit -> Ordering

(<) :: PrologRule lit -> PrologRule lit -> Bool

(<=) :: PrologRule lit -> PrologRule lit -> Bool

(>) :: PrologRule lit -> PrologRule lit -> Bool

(>=) :: PrologRule lit -> PrologRule lit -> Bool

max :: PrologRule lit -> PrologRule lit -> PrologRule lit

min :: PrologRule lit -> PrologRule lit -> PrologRule lit

renamerule :: forall lit atom term v. (IsLiteral lit, JustLiteral lit, Ord lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Int -> PrologRule lit -> (PrologRule lit, Int)

testProlog :: Test