Data.Logic.ATP.Herbrand

Relation between FOL and propositonal logic; Herbrand theorem.

Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

Documentation

pholds :: JustPropositional pf => (AtomOf pf -> Bool) -> pf -> Bool

Propositional valuation.

herbfuns :: (atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, IsFormula fof, HasApply atom, Ord function) => fof -> (Set (function, Arity), Set (function, Arity))

Get the constants for Herbrand base, adding nullary one if necessary.

groundterms :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Arity) -> Int -> Set term

Enumeration of ground terms and m-tuples, ordered by total fns.

groundtuples :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Int) -> Int -> Int -> Set [term]

herbloop :: forall lit atom function v term. (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, HasApply atom, IsTerm term) => (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)) -> (Set (Set lit) -> Bool) -> Set (Set lit) -> Set term -> Set (function, Int) -> [TVarOf term] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Set [term]

Iterate modifier "mfn" over ground terms till "tfn" fails.

gilmore_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit, HasApply atom, IsTerm term) => Set (Set lit) -> Set term -> Set (function, Int) -> [TVarOf term] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Set [term]

Hence a simple Gilmore-type procedure.

gilmore :: forall fof atom term v function. (IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> Int

test01 :: Test

First example and a little tracing.

p24 :: Test

p45fm :: Formula

Slightly less easy example. Expected output:

0 ground instances tried; 1 items in list 0 ground instances tried; 1 items in list 1 ground instances tried; 13 items in list 1 ground instances tried; 13 items in list 2 ground instances tried; 57 items in list 3 ground instances tried; 84 items in list 4 ground instances tried; 405 items in list

p45 :: Test

dp_mfn :: Ord b => Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)

The Davis-Putnam procedure for first order logic.

dp_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit, HasApply atom, IsTerm term) => Set (Set lit) -> Set term -> Set (function, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Set [term]

davisputnam :: forall formula atom term v function. (IsFirstOrder formula, Ord formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int

davisputnam' :: forall formula atom term v function. (IsFirstOrder formula, Ord formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> formula -> formula -> Int

Show how few of the instances we really need. Hence unification!

dp_refine_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit, IsTerm term, HasApply atom) => Set (Set lit) -> Set term -> Set (function, Int) -> [v] -> Int -> Set (Set lit) -> Set [term] -> Set [term] -> Set [term]

Try to cut out useless instantiations in final result.

dp_refine :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, HasApply atom, JustLiteral lit, Ord lit, IsTerm term) => Set (Set lit) -> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]

testHerbrand :: Test