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)

Ord lit => Ord (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