Here is one possible approach. First, convert the propositional
formula into the conjunctive normal form (disjunctive will work just
as well). Recall, the conjunctive normal form (CNF) is
type CNF = [Clause]
type Clause = [Literal]
data Literal = Pos PropLetter | Neg PropLetter
type PropLetter -- String or other representation for atomic propositions
We assume that clauses in CNF are ordered and can be identified by
natural indices.
A CNF can be stored in the following table:
CREATE DOMAIN PropLetter ...
CREATE TYPE occurrence AS (
clause_number integer, (* index of a clause *)
clause_card integer, (* number of literals in that clause *)
positive boolean (* whether a positive or negative occ *)
);
CREATE TABLE Formula (
prop_letter PropLetter references (table_of_properties),
occurrences occurrence[]
);
That is, for each prop letter we indicate which clause it occurs in
(as a positive or a negative literal) and how many literals in that
clause. The latter number (clause cardinality) can be factored out if
we are orthodox. Since a letter may occur in many clauses, we use
PostgreSQL arrays (which are now found in many DBMS).
The formula can be evaluated incrementally: by fetching the rows one
by one, keeping track of not yet decided clauses. We can stop as soon
as we found a clause that evaluates to FALSE.
BTW, `expression problem' typically refers to something else entirely
(how to embed a language and be able to add more syntactic forms to
the language and more evaluators without breaking previously written
code).
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
