Calculemus contains functions to perform formal deductive inference in
propositional or first order logic.
This document demonstrates how to use this library.
First, we reference and open Calculemus
#r "nuget: Calculemus, 1.0.6"
open Calculemus
Then, it is necessary to load the module for the type of logical objects we are going to work with
open Fol
and also convenient to setup the corresponding custom printers
fsi.AddPrinter sprint_fol_formula
Now, to create a formula, let's say first order, it is necessary to apply the parser to the desired string expression.
let fm = !!"exists x. forall y z. (P(y) ==> Q(z)) ==> P(x) ==> Q(x)"
The library contains various procedures to prove propositional tautologies or first order valid formulas. Note that, depending on the complexity of the formulas involved, these procedures may or may not be able to complete the task.
To try an automatic proof, it is enough to load the module containing it and apply the function to the desired formula.
The functions for tautology checking of propositional formulas return true or false, depending if the formula is a tautology or not:
open Prop
open DP
dplbtaut !>"(p ==> q) <=> (~q ==> ~p)"
Unlike propositional logic, for first order logic automated validity checking is only semidecidable. There are methods that, given a valid formula, can generate a sequence of inferences such that after a finite (but not definable in advance) number of steps prove the validity of the formula. However, if the formula is not valid, the same procedures will continue ad infinitum without returning any result. This is not simply a question of how well designed such procedures are but the best that can be hoped also from a theoretical point of view.
Thus, the automated validity checking functions for first order logic, in general, don't return a simple true or false but rather the information that the procedure ended successfully or, in some cases, that it was interrupted and therefore did not produce any significant results.
For example, Herbrand.davisputnam
open Herbrand
let test = davisputnam fm
0 ground instances tried; 0 items in list.
0 ground instances tried; 0 items in list.
1 ground instances tried; 3 items in list.
1 ground instances tried; 3 items in list.
2 ground instances tried; 6 items in list.
val test: int = 3
|
as the api reference reports, returns
The number of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops indefinitely till the memory is full.
The library contains also various interactive theorem proving features in the LCF styles, both with simple forward rules (starting from axioms and deriving new theorems by applying inference rules); as with goal oriented proofs based on tactics.
open Lcf
open Lcfprop
open Folderived
open Tactics
Like before is convenient to install the custom printers:
fsi.AddPrinter sprint_thm
fsi.AddPrinter sprint_goal
axiom_addimp !!"P(x)" !!"Q(x)" // |- P(x) ==> Q(x) ==> P(x)
|> add_assum !!"R(x,y)" // |- R(x,y) ==> P(x) ==> Q(x) ==> P(x)
let g0 =
!! @"
(forall x. x <= x) /\
(forall x y z. x <= y /\ y <= z ==> x <= z) /\
(forall x y. f(x) <= y <=> x <= g(y))
==> (forall x y. x <= y ==> f(x) <= f(y)) /\
(forall x y. x <= y ==> g(x) <= g(y))"
|> set_goal
g0 |> print_goal
1 subgoal:
---> (forall x. x <= x) /\ (forall x y z. x <= y /\ y <= z ==> x <= z) /\ (forall x y. f(x) <= y <=> x <= g(y)) ==> (forall x y. x <= y ==> f(x) <= f(y)) /\ (forall x y. x <= y ==> g(x) <= g(y))
|
let g1 = imp_intro_tac "ant" g0
g1 |> print_goal
1 subgoal:
ant: (forall x. x <= x) /\ (forall x y z. x <= y /\ y <= z ==> x <= z) /\ (forall x y. f(x) <= y <=> x <= g(y))
---> (forall x y. x <= y ==> f(x) <= f(y)) /\ (forall x y. x <= y ==> g(x) <= g(y))
|
let g2 = conj_intro_tac g1
g2 |> print_goal
2 subgoals starting with
ant: (forall x. x <= x) /\ (forall x y z. x <= y /\ y <= z ==> x <= z) /\ (forall x y. f(x) <= y <=> x <= g(y))
---> forall x y. x <= y ==> f(x) <= f(y)
|
let g3 = Lib.Function.funpow 2 (auto_tac by ["ant"]) g2
g3 |> print_goal
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Searching with depth limit 5
Searching with depth limit 6
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Searching with depth limit 5
Searching with depth limit 6
No subgoals
|
extract_thm g3
|> print_thm
|- (forall x. x <= x) /\ (forall x y z. x <= y /\ y <= z ==> x <= z) /\ (forall x y. f(x) <= y <=> x <= g(y)) ==> (forall x y. x <= y ==> f(x) <= f(y)) /\ (forall x y. x <= y ==> g(x) <= g(y))
|
[note("eq_sym",(!!"forall x y. x = y ==> y = x"))
using [eq_sym (!!!"x") (!!!"y")];
note("eq_trans",(!!"forall x y z. x = y /\ y = z ==> x = z"))
using [eq_trans (!!!"x") (!!!"y") (!!!"z")];
note("eq_cong",(!!"forall x y. x = y ==> f(x) = f(y)"))
using [axiom_funcong "f" [(!!!"x")] [(!!!"y")]];
assume ["le",(!!"forall x y. x <= y <=> x * y = x");
"hom",(!!"forall x y. f(x * y) = f(x) * f(y)")];
fix "x"; fix "y";
assume ["xy",(!!"x <= y")];
so have (!!"x * y = x") by ["le"];
so have (!!"f(x * y) = f(x)") by ["eq_cong"];
so have (!!"f(x) = f(x * y)") by ["eq_sym"];
so have (!!"f(x) = f(x) * f(y)") by ["eq_trans"; "hom"];
so have (!!"f(x) * f(y) = f(x)") by ["eq_sym"];
so conclude (!!"f(x) <= f(y)") by ["le"];
qed]
|> prove !! @"
(forall x y. x <= y <=> x * y = x) /\
(forall x y. f(x * y) = f(x) * f(y))
==> forall x y. x <= y ==> f(x) <= f(y)"
|> print_thm
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Searching with depth limit 5
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
|- (forall x y. x <= y <=> x * y = x) /\ (forall x y. f(x * y) = f(x) * f(y)) ==> (forall x y. x <= y ==> f(x) <= f(y))
|
namespace Calculemus
module Fol
from Calculemus
<summary>
Basic stuff for first order logic: datatype, parsing and printing,
semantics, syntax operations and substitution.
</summary>
<category index="4">First order logic</category>
val fm: Formulas.formula<fol>
module Prop
from Calculemus
<summary>
Basic stuff for propositional logic: datatype, parsing and prettyprinting,
syntax and semantics, normal forms.
</summary>
<note>
Although this module defines a specific type
<see cref="T:Calculemus.Prop.prop" /> for primitive propositions, most of
the functions defined here for propositional logic are applicable (and
intended to be applied) in general to any kind of
<see cref="T:Calculemus.Formulas.formula`1" /> and in particular
to our specific type of first order logic formulas
<see cref="T:Calculemus.FolModule.fol" />. These functions handle symbolic
computation at the propositional level for any kind of
<see cref="T:Calculemus.Formulas.formula`1" /> unless the signature
restricts them to the <see cref="T:Calculemus.Prop.prop" /> type.
<p></p>
As remarked in the handbook, the defined type
<see cref="T:Calculemus.Prop.prop" /> for propositional variables is fixed
here just to make experimentation with some of the operations easier.
</note>
<category index="3">Propositional logic</category>
module DP
from Calculemus
<summary>
The Davis-Putnam and the Davis-Putnam-Loveland-Logemann procedures.
</summary>
<category index="3">Propositional logic</category>
val dplbtaut: fm: Formulas.formula<prop> -> bool
<summary>
Tests <c>fm</c> (propositional) validity with the
Davis-Putnam-Loveland-Logemann procedure with iterative implementation
and backjumping and learning optimizations.
</summary>
<param name="fm">The input formula.</param>
<returns>
true, if the input formula is a tautology: otherwise false.
</returns>
<example id="dplbtaut-1"><code lang="fsharp">
dplbtaut !> "p"
</code>
Evaluates to <c>false</c>.
</example>
<example id="dplbtaut-2"><code lang="fsharp">
dplbtaut (prime 11)
</code>
Evaluates to <c>true</c>.
</example>
<example id="dplbtaut-3">
dplbtaut is 4X more faster than dplitaut:
<code lang="fsharp">
time dplbtaut (prime 101)
// Evaluates to:
// CPU time (user): 36.981689
// val it: bool = true
time dplitaut (prime 101)
// Evaluates to:
// CPU time (user): 130.045742
// val it: bool = true
</code></example>
<category index="8">DPLL with backjumping and learning</category>
module Herbrand
from Calculemus
<summary>
Relation between first order and propositional logic; Herbrand theorem.
</summary>
<category index="4">First order logic</category>
val test: int
val davisputnam: fm: Formulas.formula<fol> -> int
<summary>
Tests the validity of a formula with the Davis-Putnam procedure.
</summary>
<param name="fm">The input formula.</param>
<returns>
The number of ground tuples generated and prints to the <c>stdout</c>
how many ground instances were tried, if the procedure terminates (thus
indicating that the formula is valid); otherwise, loops indefinitely
till the memory is full.
</returns>
<example id="davisputnam-1"><code lang="fsharp">
davisputnam !! "exists x. forall y. P(x) ==> P(y)"
</code>
Evaluates to <c>2</c> and print to the <c>stdout</c>:
<code lang="fsharp">
0 ground instances tried; 0 items in list.
0 ground instances tried; 0 items in list.
1 ground instances tried; 2 items in list.
1 ground instances tried; 2 items in list.
</code></example>
<note>
The procedure loops infinitely if the initial formula is not valid and
even if it is, it is not guaranteed to end.
</note>
<category index="5">The Davis-Putnam procedure for first order logic</category>
module Lcf
from Calculemus
<summary>
LCF-style system for first order logic.
</summary>
<remarks>
Basic first order deductive system.
<p></p>
This is based on Tarski's trick for avoiding use of a substitution
primitive. It seems about the simplest possible system we could use.
</remarks>
<category index="7">Interactive theorem proving</category>
module Lcfprop
from Calculemus
<summary>
Propositional logic by inference.
</summary>
<category index="7">Interactive theorem proving</category>
module Folderived
from Calculemus
<summary>
First-order reasoning by inference.
</summary>
<category index="7">Interactive theorem proving</category>
module Tactics
from Calculemus
<summary>
Tactics and Mizar-style proofs.
</summary>
<category index="7">Interactive theorem proving</category>
val axiom_addimp: p: Formulas.formula<fol> -> q: Formulas.formula<fol> -> thm
<summary>
|- p -> (q -> p)
</summary>
val add_assum: p: Formulas.formula<fol> -> th: thm -> thm
val g0: goals
val set_goal: p: Formulas.formula<fol> -> goals
val print_goal: g: goals -> unit
val g1: goals
val imp_intro_tac: s: string -> gls: goals -> goals
val g2: goals
val conj_intro_tac: gls: goals -> goals
val g3: goals
namespace Calculemus.Lib
module Function
from Calculemus.Lib
<namespacedoc><summary>
Basic library for the global implementation.
</summary></namespacedoc>
<summary>Functions over predicates and functions.</summary>
<category index="1">Functions over predicates and functions</category>
val funpow: n: int -> f: ('a -> 'a) -> x: 'a -> 'a
<summary>
Iterates the application of a function <c>f</c> to an argument <c>x</c>
a fixed number <c>n</c> of times.
</summary>
<remarks><c>funpow n f x</c> applies <c>f</c> to <c>x</c> for <c>n</c> times,
giving the result <c>f (f ... (f x)...)</c> where the number of
<c>f</c>'s is <c>n</c>. <c>funpow 0 f x</c> returns <c>x</c>. If
<c>n</c> is negative, it is treated as <c>0</c>. It fails, if any of
the <c>n</c> applications of <c>f</c> fail.
</remarks>
<param name="n">The number of times to apply the function.</param>
<param name="f">The function to apply.</param>
<param name="x">The element to apply the function to.</param>
<returns>
The result of applying <c>f</c> to <c>x</c> for <c>n</c> times, if
<c>n</c> is >= 0. Otherwise, the input argument <c>x</c> unchanged.
</returns>
<example id="funpow-1"><code lang="fsharp">
2. |> funpow 2 (fun x -> x ** 2.)
</code>
Evaluates to <c>16.</c></example>
<example id="funpow-2"><code lang="fsharp">
2. |> funpow 0 (fun x -> x ** 2.)
</code>
Evaluates to <c>2.</c></example>
<example id="funpow-3"><code lang="fsharp">
2. |> funpow -1 (fun x -> x ** 2.)
</code>
Evaluates to <c>2.</c></example>
<example id="funpow-4"><code lang="fsharp">
2. |> funpow 2 ((/) 0)
</code>
Throws <c>System.DivideByZeroException:
Attempted to divide by zero.</c></example>
val auto_tac: byfn: ('a -> Formulas.formula<fol> -> goals -> thm list) -> hyps: 'a -> g: goals -> goals
val by: hyps: string list -> p: 'a -> gls: goals -> thm list
val extract_thm: gls: goals -> thm
val print_thm: th: thm -> unit
<summary>
A printer for theorems
</summary>
val note: l: string * p: Formulas.formula<fol> -> (('a -> Formulas.formula<fol> -> goals -> thm list) -> 'a -> goals -> goals)
val using: ths: thm list -> p: 'a -> g: goals -> thm list
val eq_sym: s: term -> t: term -> thm
val eq_trans: s: term -> t: term -> u: term -> thm
val axiom_funcong: f: string -> lefts: term list -> rights: term list -> thm
<summary>
|- s1 = t1 -> ... -> sn = tn -> f(s1, ..., sn) = f(t1, ..., tn)
</summary>
val assume: lps: (string * Formulas.formula<fol>) list -> gls: goals -> goals
val fix: (string -> goals -> goals)
val so: tac: ('a -> ('b -> 'c -> goals -> thm list) -> 'd) -> arg: 'a -> byfn: ('b -> 'c -> goals -> thm list) -> 'd
val have: p: Formulas.formula<fol> -> (('a -> Formulas.formula<fol> -> goals -> thm list) -> 'a -> goals -> goals)
val conclude: p: Formulas.formula<fol> -> byfn: ('a -> Formulas.formula<fol> -> goals -> thm list) -> hyps: 'a -> gl: goals -> goals
val qed: gl: goals -> goals
val prove: p: Formulas.formula<fol> -> prf: (goals -> goals) list -> thm