{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Logic.ATP.Herbrand where
import Data.Logic.ATP.Apply (functions, HasApply(TermOf))
import Data.Logic.ATP.DP (dpll)
import Data.Logic.ATP.FOL (IsFirstOrder, lsubst, fv, generalize)
import Data.Logic.ATP.Formulas (IsFormula(AtomOf), overatoms, atomic)
import Data.Logic.ATP.Lib (allpairs, distrib)
import Data.Logic.ATP.Lit ((.~.), JustLiteral, LFormula)
import Data.Logic.ATP.Parser(fof)
import Data.Logic.ATP.Pretty (prettyShow)
import Data.Logic.ATP.Prop (eval, JustPropositional, PFormula, simpcnf, simpdnf, trivial)
import Data.Logic.ATP.Skolem (Formula, HasSkolem(SVarOf), runSkolem, skolemize)
import Data.Logic.ATP.Term (Arity, IsTerm(TVarOf, FunOf), fApp)
import qualified Data.Map.Strict as Map
import Data.Set as Set
import Data.String (IsString(..))
import Debug.Trace
import Test.HUnit hiding (tried)
pholds :: (JustPropositional pf) => (AtomOf pf -> Bool) -> pf -> Bool
pholds :: forall pf.
JustPropositional pf =>
(AtomOf pf -> Bool) -> pf -> Bool
pholds AtomOf pf -> Bool
d pf
fm = pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
fm AtomOf pf -> Bool
d
herbfuns :: (atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, IsFormula fof, HasApply atom, Ord function) => fof -> (Set (function, Arity), Set (function, Arity))
herbfuns :: forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns fof
fm =
let (Set (function, Int)
cns,Set (function, Int)
fns) = ((function, Int) -> Bool)
-> Set (function, Int)
-> (Set (function, Int), Set (function, Int))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (\ (function
_,Int
ar) -> Int
ar Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (fof -> Set (function, Int)
forall formula atom function term.
(IsFormula formula, HasApply atom, Ord function,
atom ~ AtomOf formula, term ~ TermOf atom,
function ~ FunOf term) =>
formula -> Set (function, Int)
functions fof
fm) in
if Set (function, Int) -> Bool
forall a. Set a -> Bool
Set.null Set (function, Int)
cns then ((function, Int) -> Set (function, Int)
forall a. a -> Set a
Set.singleton (String -> function
forall a. IsString a => String -> a
fromString String
"c",Int
0),Set (function, Int)
fns) else (Set (function, Int)
cns,Set (function, Int)
fns)
groundterms :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Arity) -> Int -> Set term
groundterms :: forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Set term
groundterms Set term
cntms Set (f, Int)
_ Int
0 = Set term
cntms
groundterms Set term
cntms Set (f, Int)
fns Int
n =
((f, Int) -> Set term -> Set term)
-> Set term -> Set (f, Int) -> Set term
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (f, Int) -> Set term -> Set term
terms Set term
forall a. Set a
Set.empty Set (f, Int)
fns
where
terms :: (f, Int) -> Set term -> Set term
terms (f
f,Int
m) Set term
l = Set term -> Set term -> Set term
forall a. Ord a => Set a -> Set a -> Set a
Set.union (([term] -> term) -> Set [term] -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp f
FunOf term
f) (Set term -> Set (f, Int) -> Int -> Int -> Set [term]
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
cntms Set (f, Int)
fns (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
m)) Set term
l
groundtuples :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples :: forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
_ Set (f, Int)
_ Int
0 Int
0 = [term] -> Set [term]
forall a. a -> Set a
Set.singleton []
groundtuples Set term
_ Set (f, Int)
_ Int
_ Int
0 = Set [term]
forall a. Set a
Set.empty
groundtuples Set term
cntms Set (f, Int)
fns Int
n Int
m =
(Int -> Set [term] -> Set [term])
-> Set [term] -> Set Int -> Set [term]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Int -> Set [term] -> Set [term]
tuples Set [term]
forall a. Set a
Set.empty ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
0 .. Int
n])
where
tuples :: Int -> Set [term] -> Set [term]
tuples Int
k Set [term]
l = Set [term] -> Set [term] -> Set [term]
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((term -> [term] -> [term]) -> Set term -> Set [term] -> Set [term]
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (:) (Set term -> Set (f, Int) -> Int -> Set term
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Set term
groundterms Set term
cntms Set (f, Int)
fns Int
k) (Set term -> Set (f, Int) -> Int -> Int -> Set [term]
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
cntms Set (f, Int)
fns (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))) Set [term]
l
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]
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]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit) -> Bool
tfn Set (Set lit)
fl0 Set term
cntms Set (function, Int)
fns [TVarOf term]
fvs Int
n Set (Set lit)
fl Set [term]
tried Set [term]
tuples =
let debug :: Set [term] -> Set [term]
debug Set [term]
x = String -> Set [term] -> Set [term]
forall a. String -> a -> a
trace (Int -> String
forall a. Show a => a -> String
show (Set [term] -> Int
forall a. Set a -> Int
size Set [term]
tried) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ground instances tried; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Set (Set lit) -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set (Set lit)
fl) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" items in list") Set [term]
x in
case Set [term] -> Maybe ([term], Set [term])
forall a. Set a -> Maybe (a, Set a)
Set.minView (Set [term] -> Set [term]
debug Set [term]
tuples) of
Maybe ([term], Set [term])
Nothing ->
let newtups :: Set [term]
newtups = Set term -> Set (function, Int) -> Int -> Int -> Set [term]
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
cntms Set (function, Int)
fns Int
n ([v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [v]
[TVarOf term]
fvs) in
(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]
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]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit) -> Bool
tfn Set (Set lit)
fl0 Set term
cntms Set (function, Int)
fns [TVarOf term]
fvs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Set (Set lit)
fl Set [term]
tried Set [term]
newtups
Just ([term]
tup, Set [term]
tups) ->
let fpf' :: Map v term
fpf' = [(v, term)] -> Map v term
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([v] -> [term] -> [(v, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
[TVarOf term]
fvs [term]
tup) in
let fl' :: Set (Set lit)
fl' = Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit)
fl0 (Map v term -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst Map v term
fpf') Set (Set lit)
fl in
if Bool -> Bool
not (Set (Set lit) -> Bool
tfn Set (Set lit)
fl') then [term] -> Set [term] -> Set [term]
forall a. Ord a => a -> Set a -> Set a
Set.insert [term]
tup Set [term]
tried
else (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]
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]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit) -> Bool
tfn Set (Set lit)
fl0 Set term
cntms Set (function, Int)
fns [TVarOf term]
fvs Int
n Set (Set lit)
fl' ([term] -> Set [term] -> Set [term]
forall a. Ord a => a -> Set a -> Set a
Set.insert [term]
tup Set [term]
tried) Set [term]
tups
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]
gilmore_loop :: forall atom lit term function v.
(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]
gilmore_loop =
(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]
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]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
forall {lit} {a}.
(IsLiteral lit, Ord lit) =>
Set (Set a) -> (a -> lit) -> Set (Set lit) -> Set (Set lit)
mfn (Bool -> Bool
not (Bool -> Bool) -> (Set (Set lit) -> Bool) -> Set (Set lit) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set lit) -> Bool
forall a. Set a -> Bool
Set.null)
where
mfn :: Set (Set a) -> (a -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set a)
djs0 a -> lit
ifn Set (Set lit)
djs = (Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set lit -> Bool) -> Set lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set lit -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) (Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib ((Set a -> Set lit) -> Set (Set a) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((a -> lit) -> Set a -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> lit
ifn) Set (Set a)
djs0) Set (Set lit)
djs)
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
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
gilmore fof
fm =
let (PFormula atom
sfm :: PFormula atom) = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf fof -> AtomOf (PFormula atom))
-> fof -> SkolemT Identity function (PFormula atom)
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.) (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm))) in
let fvs :: [v]
fvs = Set v -> [v]
forall a. Set a -> [a]
Set.toList ((AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ AtomOf (PFormula atom)
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set v
s (fof -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf fof -> fof
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf fof
AtomOf (PFormula atom)
a :: fof))) PFormula atom
sfm (Set v
forall a. Set a
Set.empty))
(Set (function, Int)
consts,Set (function, Int)
fns) = PFormula atom -> (Set (function, Int), Set (function, Int))
forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns PFormula atom
sfm in
let cntms :: Set term
cntms = ((function, Int) -> term) -> Set (function, Int) -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ (function
c,Int
_) -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
c []) Set (function, Int)
consts in
Set [term] -> Int
forall a. Set a -> Int
Set.size (Set (Set (LFormula atom))
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set (LFormula atom))
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(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]
gilmore_loop ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
sfm :: Set (Set (LFormula atom))) Set term
cntms Set (function, Int)
fns ([v]
[TVarOf term]
fvs) Int
0 (Set (LFormula atom) -> Set (Set (LFormula atom))
forall a. a -> Set a
Set.singleton Set (LFormula atom)
forall a. Set a
Set.empty) Set [term]
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty)
test01 :: Test
test01 :: Test
test01 =
let fm :: Formula
fm = [fof| exists x. (forall y. p(x) ==> p(y)) |]
expected :: Int
expected = Int
2
in
Assertion -> Test
TestCase (HasCallStack => String -> Assertion
String -> Assertion
assertString (case Formula -> Int
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
gilmore Formula
fm of
Int
r | Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
expected -> String
""
Int
r -> String
"gilmore(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
fm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
expected))
p24 :: Test
p24 :: Test
p24 =
let label :: String
label = String
"gilmore p24 (p. 160): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
fm
fm :: Formula
fm = [fof|~(exists x. (U(x) & Q(x))) &
(forall x. (P(x) ==> Q(x) | R(x))) &
~(exists x. (P(x) ==> (exists x. Q(x)))) &
(forall x. (Q(x) & R(x) ==> U(x)))
==> (exists x. (P(x) & R(x)))|] in
String -> Test -> Test
TestLabel String
label (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Int -> Int -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
label Int
1 (Formula -> Int
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
gilmore Formula
fm)
p45fm :: Formula
p45fm :: Formula
p45fm = [fof| (((forall x.
((P(x) & (forall y. ((G(y) & H(x,y)) ==> J(x,y)))) ==>
(forall y. ((G(y) & H(x,y)) ==> R(y))))) &
((~(exists y. (L(y) & R(y)))) &
(exists x.
(P(x) &
((forall y. (H(x,y) ==> L(y))) &
(forall y. ((G(y) & H(x,y)) ==> J(x,y)))))))) ==>
(exists x. (P(x) & (~(exists y. (G(y) & H(x,y))))))) |]
p45 :: Test
p45 :: Test
p45 = String -> Test -> Test
TestLabel String
"gilmore p45" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Int -> Int -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"gilmore p45" Int
5 (Formula -> Int
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
gilmore Formula
p45fm)
dp_mfn :: Ord b => Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn :: forall b a.
Ord b =>
Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn Set (Set a)
cjs0 a -> b
ifn Set (Set b)
cjs = Set (Set b) -> Set (Set b) -> Set (Set b)
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((Set a -> Set b) -> Set (Set a) -> Set (Set b)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((a -> b) -> Set a -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> b
ifn) Set (Set a)
cjs0) Set (Set b)
cjs
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]
dp_loop :: forall atom lit term function v.
(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]
dp_loop = (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]
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]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
forall b a.
Ord b =>
Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll
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 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
davisputnam formula
fm =
let (PFormula atom
sfm :: PFormula atom) = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf formula -> AtomOf (PFormula atom))
-> formula -> SkolemT Identity function (PFormula atom)
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize atom -> atom
AtomOf formula -> AtomOf (PFormula atom)
forall a. a -> a
id (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) in
let fvs :: [v]
fvs = Set v -> [v]
forall a. Set a -> [a]
Set.toList ((AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ AtomOf (PFormula atom)
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
AtomOf (PFormula atom)
a :: formula)) Set v
s) PFormula atom
sfm Set v
forall a. Set a
Set.empty)
(Set (function, Int)
consts,Set (function, Int)
fns) = PFormula atom -> (Set (function, Int), Set (function, Int))
forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns PFormula atom
sfm in
let cntms :: Set term
cntms = ((function, Int) -> term) -> Set (function, Int) -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ (function
c,Int
_) -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
c []) Set (function, Int)
consts in
Set [term] -> Int
forall a. Set a -> Int
Set.size (Set (Set (LFormula atom))
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set (LFormula atom))
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(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]
dp_loop ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
sfm :: Set (Set (LFormula atom))) Set term
cntms Set (function, Int)
fns [v]
fvs Int
0 Set (Set (LFormula atom))
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty)
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
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
davisputnam' formula
_ formula
_ formula
fm =
let (PFormula atom
sfm :: PFormula atom) = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf formula -> AtomOf (PFormula atom))
-> formula -> SkolemT Identity function (PFormula atom)
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize atom -> atom
AtomOf formula -> AtomOf (PFormula atom)
forall a. a -> a
id (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) in
let fvs :: [v]
fvs = Set v -> [v]
forall a. Set a -> [a]
Set.toList ((AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ (AtomOf formula
a :: AtomOf formula) Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
a :: formula)) Set v
s) PFormula atom
sfm Set v
forall a. Set a
Set.empty)
consts :: Set (function, Arity)
fns :: Set (function, Arity)
(Set (function, Int)
consts,Set (function, Int)
fns) = PFormula atom -> (Set (function, Int), Set (function, Int))
forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns PFormula atom
sfm in
let cntms :: Set (TermOf (AtomOf formula))
cntms :: Set (TermOf (AtomOf formula))
cntms = ((function, Int) -> term) -> Set (function, Int) -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ (function
c,Int
_) -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
c []) Set (function, Int)
consts in
Set [term] -> Int
forall a. Set a -> Int
Set.size (Set (Set (LFormula atom))
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set (LFormula atom))
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(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]
dp_refine_loop ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
sfm :: Set (Set (LFormula atom))) Set term
Set (TermOf (AtomOf formula))
cntms Set (function, Int)
fns [v]
fvs Int
0 Set (Set (LFormula atom))
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty)
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]
dp_refine_loop :: forall atom lit term function v.
(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]
dp_refine_loop Set (Set lit)
cjs0 Set term
cntms Set (function, Int)
fns [v]
fvs Int
n Set (Set lit)
cjs Set [term]
tried Set [term]
tuples =
let tups :: Set [term]
tups = Set (Set lit)
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(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]
dp_loop Set (Set lit)
cjs0 Set term
cntms Set (function, Int)
fns [v]
fvs Int
n Set (Set lit)
cjs Set [term]
tried Set [term]
tuples in
Set (Set lit)
-> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
forall atom lit term v.
(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]
dp_refine Set (Set lit)
cjs0 [v]
[TVarOf term]
fvs Set [term]
tups Set [term]
forall a. Set a
Set.empty
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]
dp_refine :: forall atom lit term v.
(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]
dp_refine Set (Set lit)
cjs0 [TVarOf term]
fvs Set [term]
dknow Set [term]
need =
case Set [term] -> Maybe ([term], Set [term])
forall a. Set a -> Maybe (a, Set a)
Set.minView Set [term]
dknow of
Maybe ([term], Set [term])
Nothing -> Set [term]
need
Just ([term]
cl, Set [term]
dknow') ->
let mfn :: [term] -> Set (Set lit) -> Set (Set lit)
mfn = Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
forall b a.
Ord b =>
Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn Set (Set lit)
cjs0 ((lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> ([term] -> lit -> lit)
-> [term]
-> Set (Set lit)
-> Set (Set lit)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v term -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst (Map v term -> lit -> lit)
-> ([term] -> Map v term) -> [term] -> lit -> lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(v, term)] -> Map v term
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(v, term)] -> Map v term)
-> ([term] -> [(v, term)]) -> [term] -> Map v term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [v] -> [term] -> [(v, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
[TVarOf term]
fvs in
let flag :: Bool
flag = Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll (([term] -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set [term] -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold [term] -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit)
forall a. Set a
Set.empty (Set [term] -> Set [term] -> Set [term]
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set [term]
need Set [term]
dknow')) in
Set (Set lit)
-> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
forall atom lit term v.
(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]
dp_refine Set (Set lit)
cjs0 [TVarOf term]
fvs Set [term]
dknow' (if Bool
flag then [term] -> Set [term] -> Set [term]
forall a. Ord a => a -> Set a -> Set a
Set.insert [term]
cl Set [term]
need else Set [term]
need)
testHerbrand :: Test
testHerbrand :: Test
testHerbrand = String -> Test -> Test
TestLabel String
"Herbrand" ([Test] -> Test
TestList [Test
test01, Test
p24, Test
p45])