oleg | 24 Jul 07:42 2013

Expression problem in the database?

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 *)

  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
(Continue reading)