Problems.P53

Description

Part of Ninety-Nine Haskell Problems. Some solutions are in Solutions.P53.

Synopsis

# Documentation

isTheorem :: [Formula] -> Formula -> Bool Source #

In propositional logic, if a formula $$X$$ is always true when a set of axioms $$\mathrm{S}$$ are true, then $$X$$ is said to be valid given $$\mathrm{S}$$.

The resolution rule is an inference rule in propositional logic where two clauses with complementary literals can be merged to produce another clause. Specifically, if clauses $$x \vee a_1 \vee \ldots \vee a_m$$ and $$\neg x \vee b_1 \vee \ldots \vee b_n$$ are true, then the clause $$a_1 \vee \ldots \vee a_m \vee b_1 \vee \ldots \vee b_n$$ must also be true. This is commonly expressed as

$x \vee a_1 \vee \ldots \vee a_m \hspace{2em} \neg x \vee b_1 \vee \ldots \vee b_n \above 1pt a_1 \vee \ldots \vee a_m \vee b_1 \vee \ldots \vee b_n$

The resolution rule can be used with conjunctive normal forms to prove whether or not a given formula $$X$$ is valid given a set of axioms $$\mathrm{S}$$. It is a proof by contradiction, and the procedure is as follows:

1. Conjunctively connect the formulas in $$\mathrm{S}$$ and the negation of $$X$$ into a single formula $$Y$$.

For example, if the axioms are $$x$$ and $$y$$, and the given formula is $$z$$, then $$Y$$ would be $$x \wedge y \wedge \neg z$$.

• Do not apply the resolution rule to the values of true and false. If $$Y$$ contains raw true or false values, transform $$Y$$ into a form which contains none.
2. Convert $$Y$$ into conjunctive normal form; see Problems.P52.
3. If there are two clauses for which the resolution rule can be applied, add the new clause to $$Y$$ and repeat until an empty clause is inferred or if no new clauses can be added. Filter out tautologies, i.e., clauses which will always be true because it contains both a variable and its logical complement.

• If the empty clause has been inferred, then false has been inferred from $$Y$$. I.e., there is a contradiction, so $$X$$ must have been valid given the axioms $$\mathrm{S}$$.
• If no more clauses can be inferred, then $$X$$ cannot be inferred to be valid.

Given a list of axioms and a formula, use the resolution rule to determine whether the formula is valid given the axioms.

### Examples

When $$x \wedge y \wedge z$$ is true, then obviously $$x \vee y$$ is true, so

>>> :{
isTheorem
[ Variable "X", Variable "Y", Variable "Z" ] $Disjoin [ Variable "X", Variable "Y" ] :} True  When $$x \to y$$ and $$y \to z$$, or equivalently $$\neg x \vee y$$ and $$\neg y \vee z$$, then it is also the case that $$x \to z$$, so >>> :{  isTheorem [ Disjoin [ Complement$ Variable "X", Variable "Y" ]
, Disjoin [ Complement $Variable "Y", Variable "Z" ] ]$
Disjoin [ Complement $Variable "X", Variable "Z" ] :} True  Just because $$x$$ is true does not mean that $$y$$ is true, so >>> isTheorem [ Variable "X" ]$ Variable "Y"
False


If there is a contradiction, then everything is both true and false, so

>>> isTheorem [ Variable "X", Complement $Variable "X" ]$ Value False
True


data Formula Source #

Represents a boolean formula.

Constructors

 Value Bool A constant value. Variable String A variable with given name. Complement Formula Logical complement. I.e., it is true only if its clause is false. Disjoin [Formula] Disjunction. I.e., it is true if any of its clauses are true. Conjoin [Formula] Conjunction. I.e., it is true only if all of its clauses are true.

#### Instances

Instances details
 Source # Instance detailsDefined in Problems.Logic Associated Typestype Rep Formula :: Type -> Type # Methodsto :: Rep Formula x -> Formula # Source # Instance detailsDefined in Problems.Logic MethodsshowList :: [Formula] -> ShowS # Source # Instance detailsDefined in Problems.Logic Methodsrnf :: Formula -> () # Source # Instance detailsDefined in Problems.Logic Methods(==) :: Formula -> Formula -> Bool #(/=) :: Formula -> Formula -> Bool # Source # Instance detailsDefined in Problems.Logic Methods(<) :: Formula -> Formula -> Bool #(<=) :: Formula -> Formula -> Bool #(>) :: Formula -> Formula -> Bool #(>=) :: Formula -> Formula -> Bool # type Rep Formula Source # Instance detailsDefined in Problems.Logic type Rep Formula = D1 ('MetaData "Formula" "Problems.Logic" "ninetynine-1.3.0-4Xxr3hBGtJH9Ff8qb2Invo" 'False) ((C1 ('MetaCons "Value" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "Complement" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula)) :+: (C1 ('MetaCons "Disjoin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Formula])) :+: C1 ('MetaCons "Conjoin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Formula])))))