Copyright	(c) Artem Mavrin 2021
License	BSD3
Maintainer	artemvmavrin@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

AutoProof.Classical.CNF

Contents

Types
Conversion functions
Operations

Description

Functions and types related to conjunctive normal forms.

This module is intended to be imported with a qualified name, as in

import qualified AutoProof.Classical.CNF as CNF

This gives the conversion functions in this module descriptive names like CNF.fromFormula and CNF.toFormula.

Synopsis

type CNF a = Set (Clause a)
type Clause a = Map a Bool
type Literal a = (a, Bool)
fromFormula :: Ord a => Formula a -> CNF a
toFormula :: CNF a -> Formula a
canonicalCNF :: Ord a => Formula a -> Formula a
substitute :: Ord a => CNF a -> a -> Bool -> CNF a
substitutePure :: Ord a => CNF a -> a -> Bool -> CNF a
unitLiteral :: CNF a -> Maybe (Literal a)
pureLiteral :: Ord a => CNF a -> Maybe (Literal a)
getAnyLiteral :: CNF a -> Maybe (Literal a)

Types

type CNF a = Set (Clause a) Source #

Conjunctive normal form: represents a conjunction of clauses.

type Clause a = Map a Bool Source #

Represents a disjunction of literals.

type Literal a = (a, Bool) Source #

Represents either a propositional variable or its negation, depending on whether the boolean second component is True or False, respectively.

Conversion functions

fromFormula :: Ord a => Formula a -> CNF a Source #

Convert a Formula into conjunctive normal form.

Adapted from Figure 2.6 in

Samuel Mimram (2020) PROGRAM = PROOF.

toFormula :: CNF a -> Formula a Source #

Convert a conjunctive normal form representation of a formula into a formula.

canonicalCNF :: Ord a => Formula a -> Formula a Source #

Convert a formula into a canonical conjunctive normal form.

Examples

Expand

>>> import AutoProof.Internal.Formula
>>> canonicalCNF $ Or (Not (Imp (Var "a") (Var "b"))) (Var "c")
And (Or (Var "c") (Not (Var "b"))) (Or (Var "c") (Var "a"))

Operations

substitute :: Ord a => CNF a -> a -> Bool -> CNF a Source #

Substitute a truth value for a variable in a CNF formula.

(substitute a x True) and (substitute a x False) represent the substitutions \(a[\top/x]\) and \(a[\bot/x]\), respectively.

Examples

Expand

>>> a = And (Imp (Var "a") (Not (And (Var "b") (Not (Var "c"))))) (Var "a")
>>> cnf = CNF.fromFormula a
>>> cnf
fromList [fromList [("a",False),("b",False),("c",True)],fromList [("a",True)]]
>>> cnf2 = CNF.substitute cnf "a" True
>>> cnf2
fromList [fromList [("b",False),("c",True)]]
>>> a2 = CNF.toFormula cnf2
>>> a2
Or (Var "c") (Not (Var "b"))

substitutePure :: Ord a => CNF a -> a -> Bool -> CNF a Source #

Substitute a truth value for a variable that occurs as a pure literal within a CNF formula with the same polarity as the truth value. This precondition is not checked.

unitLiteral :: CNF a -> Maybe (Literal a) Source #

Obtain the literal of a unitary clause of a CNF formula, if there is one.

A unitary clause is one in which exactly one literal occurs.

pureLiteral :: Ord a => CNF a -> Maybe (Literal a) Source #

Obtain a pure literal of a CNF formula, if there is one.

A pure literal is one which only occurs with the a single polarity in the formula.

getAnyLiteral :: CNF a -> Maybe (Literal a) Source #

Obtain a literal from a CNF formula, if there is one.