Calculemus

Clause Module

Namespace: Calculemus
Assembly: Calculemus.dll

Useful functions for handling clauses.

A clause is a list of literals that, depending on the context, is to be considered as an iterated conjunction or an iterated disjunction of its literals.

Lists of clauses are used to represent formulas in disjunctive or conjunctive normal form and in the two contexts they are interpreted, respectively, as an iterated disjunction of conjunctions (each clause in this case is a conjunction) or as an iterated conjunction of disjunctions (and in this case, therefore, each clause is to be considered as the disjunction of its literals).

Note

This module is not part of the original book code and is added here for convenience.

Table of contents

Literals

Functions and values

Function or value Description

literals fm

Full Usage: literals fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> list The list of literals in the formula.

Returns the literals in a formula.

fm : formula<'a>

The input formula.

Returns: formula<'a> list

The list of literals in the formula.

Example 

 literals !!"P(x) ==> Q(x)"
Evaluates to ["`P(x)`";"`Q(x)`"].

opposites lits

Full Usage: opposites lits

Parameters:
Returns: formula<'a> list The list of literals that occur both positively and negatively in lits.

Returns literals that occur both positively and negatively in lits.

lits : formula<'a> list
Returns: formula<'a> list

The list of literals that occur both positively and negatively in lits.

Example 

 List.map (!!) ["P(x)";"Q(x)";"~P(x)"]
 |> opposites
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val map: mapping: ('T -> 'U) -> list: 'T list -> 'U list
Evaluates to ["`P(x)`"].

Parsing clauses

Functions and values

Function or value Description

!!>>xs

Full Usage: !!>>xs

Parameters:
    xs : string list list - The input list of string lists.

Returns: formula<fol> list list The list of clauses.

Parses a list of string lists into a list of formula lists. Useful when dealing with clauses.

xs : string list list

The input list of string lists.

Returns: formula<fol> list list

The list of clauses.

Note

This operator is not part of the original code and it was added here for convenience.

Example 

 !!>> [["P(x)"];["P(x)";"~Q(x)"]]
Evaluates to [[`P(x)`]; [`P(x)`; `~Q(x)`]].

Prettyprinting

Functions and values

Function or value Description

sprint_clauses clauses

Full Usage: sprint_clauses clauses

Parameters:
Returns: string list list

Prints the list of clauses rendering literals in the concrete string representation.

clauses : formula<fol> list list
Returns: string list list

Formula to clauses

Functions and values

Function or value Description

cjsToClauses fm

Full Usage: cjsToClauses fm

Parameters:
    fm : formula<'a> - The input CNF formula.

Returns: formula<'a> list list The corresponding list of clauses.

Converts a CNF formula into a list fo clauses.

fm : formula<'a>

The input CNF formula.

Returns: formula<'a> list list

The corresponding list of clauses.

Example 

 !! @"(Q(x) \/ ~R(x,y) \/ P(f(z)) /\ (~P(x) \/ Q(x)))"
 |> cjsToClauses
Evaluates to [[`Q(x)`; `~R(x,y)`; `P(f(z))`]; [`~P(x)`; `Q(x)`]].

djsToClauses fm

Full Usage: djsToClauses fm

Parameters:
    fm : formula<'a> - The input DNF formula.

Returns: formula<'a> list list The corresponding list of clauses.

Converts a DNF formula into a list fo clauses.

fm : formula<'a>

The input DNF formula.

Returns: formula<'a> list list

The corresponding list of clauses.

Example 

 !! @"(Q(x) /\ ~R(x,y) /\ P(f(z)) \/ (~P(x) /\ Q(x)))"
 |> djsToClauses
Evaluates to [[`Q(x)`; `~R(x,y)`; `P(f(z))`]; [`~P(x)`; `Q(x)`]].

Clauses to formula

Functions and values

Function or value Description

clausesToDnf cls

Full Usage: clausesToDnf cls

Parameters:
    cls : formula<'a> list list - The input clauses.

Returns: formula<'a> The corresponding DNF formula.

Converts a list of clauses into a DNF formula.

It is supposed that DNF is the intended representation.

cls : formula<'a> list list

The input clauses.

Returns: formula<'a>

The corresponding DNF formula.

Example 

 !!>>[["Q(x)"; "~R(x,y)"; "P(f(z))"]; ["~P(x)"; "Q(x)"]]
 |> clausesToDnf
Evaluates to `Q(x) /\ ~R(x,y) /\ P(f(z)) \/ ~P(x) /\ Q(x)`.