Dpfs.DavisPutnamFiniteSets

Datatype

data Atom

Davis-Putnam procedures

dpfs

dpfsAll

dpfsSat

dpfsSatAllSolutions

Rules: 1st Extension

findTrueFalse

resolveTrueFalse

findSimilarAtomUnits

substituteSimilarUnits

findUnit'

resolveUnit

findPureLiteral

resolvePureLiteral

Rules: 2nd Extension

findUnit'

resolveUnitCalculus

findSimpRule3

resolveSimpRule3

findFalse_Calculus

resolveFalse_Calculus

findSimpUnitCalculus

resolveCalculus1

findSelection2

setSplit2

Utilities

lookup'

setToInt

dpcnf

expectJust

toList'