-
-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathdefcnf.fsx
More file actions
39 lines (30 loc) · 1.65 KB
/
defcnf.fsx
File metadata and controls
39 lines (30 loc) · 1.65 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
// ========================================================================= //
// Copyright (c) 2003-2007, John Harrison. //
// Copyright (c) 2012 Eric Taucher, Jack Pappas, Anh-Dung Phan //
// (See "LICENSE.txt" for details.) //
// ========================================================================= //
#load "initialization.fsx"
open FSharpx.Books.AutomatedReasoning.lib
open FSharpx.Books.AutomatedReasoning.intro
open FSharpx.Books.AutomatedReasoning.formulas
open FSharpx.Books.AutomatedReasoning.prop
open FSharpx.Books.AutomatedReasoning.defcnf
fsi.AddPrinter sprint_prop_formula
// pg. 74
// ------------------------------------------------------------------------- //
// Example. //
// ------------------------------------------------------------------------- //
// defcnf.p001
cnf (parse_prop_formula @"p <=> (q <=> r)");;
// pg. 77
// ------------------------------------------------------------------------- //
// Example. //
// ------------------------------------------------------------------------- //
// defcnf.p002
defcnfOrig (parse_prop_formula @"(p \/ (q /\ ~r)) /\ s");;
// pg. 78
// ------------------------------------------------------------------------- //
// Examples. //
// ------------------------------------------------------------------------- //
// defcnf.p003
defcnf (parse_prop_formula @"(p \/ (q /\ ~r)) /\ s");;