Calculemus

Prolog Module

Namespace: Calculemus
Assembly: Calculemus.dll

Backchaining procedure for Horn clauses, and toy Prolog implementation.

Table of contents

Automated prover for Horn clauses

Functions and values

Function or value Description

backchain rules n k env goals

Full Usage: backchain rules n k env goals

Parameters:
    rules : (formula<fol> list * formula<fol>) list - The list of input rules.
    n : int - The maximum number of rule applications permitted.
    k : int - The counter for variables renaming.
    env : func<string, term> - An environment of mappings (represented as a finite partial function) from variables to terms, used as an accumulator for the final result of the unification procedure. .
    goals : formula<fol> list - The input goals.

Returns: func<string, term> The current instantiation env, if the list of goals is empty; otherwise, recursively searches through the rules one whose consequent can be unified with the current goal and such that the new subgoals together with the original ones can be solved under that instantiation.

Basic prover for Horn clauses.

rules : (formula<fol> list * formula<fol>) list

The list of input rules.

n : int

The maximum number of rule applications permitted.

k : int

The counter for variables renaming.

env : func<string, term>

An environment of mappings (represented as a finite partial function) from variables to terms, used as an accumulator for the final result of the unification procedure. .

goals : formula<fol> list

The input goals.

Returns: func<string, term>

The current instantiation env, if the list of goals is empty; otherwise, recursively searches through the rules one whose consequent can be unified with the current goal and such that the new subgoals together with the original ones can be solved under that instantiation.

Exception Thrown with message Too deep when n = 0.
Exception Thrown with message tryfind when the goals are not solvable, at least at the current limit.
Example 

 !!>["S(x) <= S(S(x))"] 
 |> backchain 
     [
         ([], !!"0 <= x"); 
         ([!!"x <= y"], !!"S(x) <= S(y)")
     ] 2 0 undefined
 |> graph
Evaluates to [("_0", ``x``); ("_1", ``S(x)``); ("_2", ``_1``); ("x", ``0``)].

hornify cls

Full Usage: hornify cls

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

Returns: formula<'a> list * formula<'a> The equivalent in rule format, if it exists.

Converts a raw Horn clause into a rule.

cls : formula<'a> list

The input Horn clause.

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

The equivalent in rule format, if it exists.

Exception Thrown with message non-Horn clause when cls is not an Horn clause.
Example 

 !!>["~P(x)";"Q(y)";"~T(x)"]
 |> hornify
Evaluates to ([`P(x)`; `T(x)`], `Q(y)`).

Example 

 !!>["P(x)";"Q(y)";"~T(x)"]
 |> hornify
Throws System.Exception: non-Horn clause.

hornprove fm

Full Usage: hornprove fm

Parameters:
Returns: func<string, term> * int The instantiation resulting from the backchain procedure and the level at which it succeeds, if the formula is valid and Horn clause convertible.

Tests the validity of a formula convertible in Horn clauses.

fm : formula<fol>

The input formula.

Returns: func<string, term> * int

The instantiation resulting from the backchain procedure and the level at which it succeeds, if the formula is valid and Horn clause convertible.

Exception Thrown with message non-Horn clause when fm is not convertible into a set of Horn clauses.
Note

Prints to the stdout the depth limits at which the search was carried out.

Example 

 Pelletier.p32
 |> hornprove
 |> fun (inst,level) -> 
     graph inst, level
val inst: obj
val level: obj
Evaluates to ([("_0", ``c_x``); ("_1", ``_0``); ("_2", ``_0``); ("_3", ``_2``)], 8).

Example 

 !! @"(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) 
         ==> ~(~q \/ ~q)"
 |> hornprove
Throws System.Exception: non-Horn clause.

renamerule k (asm, c)

Full Usage: renamerule k (asm, c)

Parameters:
    k : int - The counter for variables renaming.
    asm : formula<fol> list - The assumptions of the input rule.
    c : formula<fol> - The conclusion of the input rule.

Returns: (formula<fol> list * formula<fol>) * int The input rule with the variables renamed schematically starting with _k

Renames the variables in a rule schematically starting with _k.

k : int

The counter for variables renaming.

asm : formula<fol> list

The assumptions of the input rule.

c : formula<fol>

The conclusion of the input rule.

Returns: (formula<fol> list * formula<fol>) * int

The input rule with the variables renamed schematically starting with _k

Example 

 renamerule 0 (!!>["P(x)";"Q(y)"],!!"P(f(x))")
 |> graph
Evaluates to (([`P(_0)`; `Q(_1)`], `P(f(_0))`), 2).

Prolog

Functions and values

Function or value Description

parserule s

Full Usage: parserule s

Parameters:
    s : string - The input string to be parsed.

Returns: formula<fol> list * formula<fol> The rule corresponding to the input string, if this is syntactically valid.

Parses rules in a Prolog-like syntax.

s : string

The input string to be parsed.

Returns: formula<fol> list * formula<fol>

The rule corresponding to the input string, if this is syntactically valid.

Exception Thrown with message Extra material after rule when the input string isn't syntactically valid.
Example 

 "S(X) <= S(Y) :- X <= Y"
 |> parserule
Evaluates to ([`X <= Y`], `S(X) <= S(Y)`).

Example 

 "S(X) >"
 |> parserule
Throws System.Exception: Extra material after rule.

prolog rules gl

Full Usage: prolog rules gl

Parameters:
    rules : string list - The input rules.
    gl : string - The input goal.

Returns: formula<fol> list A successful goal's variables instantiation, if the goal is solvable from the rules.

Prolog interpreter.

rules : string list

The input rules.

gl : string

The input goal.

Returns: formula<fol> list

A successful goal's variables instantiation, if the goal is solvable from the rules.

Exception Thrown with message tryfind when the goal is not solvable from the rules.
Example 

 let lerules = ["0 <= X"; "S(X) <= S(Y) :- X <= Y"]
 
 prolog lerules "S(S(x)) <= S(S(S(0)))"
val lerules: string list
Evaluates to [`x = 0`].

Example 

 prolog lerules "S(0) <= 0"
Throws System.Exception: tryfind.

simpleprolog rules gl

Full Usage: simpleprolog rules gl

Parameters:
    rules : string list - The input rules.
    gl : string - The input goal.

Returns: func<string, term> The instantiation resulting from backchaining, if the goal is solvable from the rules.

Prolog interpreter without clear variable binding output.

rules : string list

The input rules.

gl : string

The input goal.

Returns: func<string, term>

The instantiation resulting from backchaining, if the goal is solvable from the rules.

Exception Thrown with message tryfind when the goal is not solvable from the rules.
Example 

 let lerules = ["0 <= X"; "S(X) <= S(Y) :- X <= Y"]
 
 simpleprolog lerules "S(S(0)) <= S(S(S(0)))"
 |> graph
val lerules: string list
Evaluates to [("_0", ``S(0)``); ("_1", ``S(S(0))``); ("_2", ``0``); ("_3", ``S(0)``); ("_4", ``_3``)].

Example 

 simpleprolog lerules "S(0) <= 0"
 |> graph
Throws System.Exception: tryfind.