Tests the validity of a formula in the AE fragment.

fm : formula<fol>

The input formula.

Returns: bool

true, if the input AE formula is valid; otherwise, if the input AE formula is invalid, false.

Example

 !! @"(forall x. P(1,x,x)) /\ (forall x. P(x,x,1)) /\
 (forall u v w x y z.
 P(x,y,u) /\ P(y,z,w) ==> (P(x,w,v) <=> P(u,z,v)))
 ==> forall a b c. P(a,b,c) ==> P(b,a,c)"
 |> aedecide

Example

 !! @"forall x. f(x) = 0"
 |> aedecide

Minimizes the scope of quantifiers in a NNF formula.

fm : formula<fol>

The input formula.

Returns: formula<fol>

A formula equivalent to the input with the scope of quantifiers minimized.

Example

 miniscope(nnf !!"exists y. forall x. P(y) ==> P(x)")

Given a variable x and a formula p transforms the formula exists x. p into an equivalent with the scope of the quantifier reduced.

x : string

The input variable.

p : formula<fol>

The input formula.

Returns: formula<fol>

The formula exists x. p transformed into an equivalent with the scope of the quantifier reduced.

Example

 !!"P(x) ==> forall y. Q(y)"
 |> pushquant "x"

Separates in an iterated conjunction those conjuncts with the given variable free from those in which is not.

The intention is to transform an existential formula of the form \(\exists x.\ p_1 \land \cdots \land p_n \) in \((\exists x.\ p_i \land \cdots \land p_j) \land (p_k \land \cdots \land p_l)\) where the \(p_i \land \cdots \land p_j\) are the those with \(x\) free and \(p_k \land \cdots \land p_l)\) are the other.

x : string

The given input variable.

cjs : formula<fol> list

The conjuncts in the existential formula.

Returns: formula<fol>

The existential formula of the conjunction of the cjs in which x is free conjuncted with the cjs in which x is not.

Example

 !!>["P(x)"; "Q(y)"; "T(y) /\ R(x,y)"; "S(z,w) ==> Q(i)"]
 |> separate "x"

Tests the validity of a formula that after applying miniscoping belongs to the AE fragment.

fm : formula<fol>

The input formula.

Returns: bool

true, if the input is a formula that after applying miniscoping belongs to the AE fragment and is valid; otherwise, false.

Example

 wang Pelletier.p20

Example

 wang !!"forall x. f(x) = 0"

Returns all 256 possible syllogisms.

Returns: formula<fol> list

Returns all 256 possible syllogisms together with the assumptions that the terms are not empty.

Returns: formula<fol> list

Returns an English reading of a premiss.

fm : formula<fol>

The input syllogism premiss.

Returns: string

An English reading of the input syllogism premiss.

Example

 premiss_A ("P", "S")
 |> anglicize_premiss

Example

 !!"P(x)"
 |> anglicize_premiss

Returns an English reading of a syllogism.

arg0 : formula<fol>

Returns: string

An English reading of the input syllogism.

Example

 premiss_A ("M", "P")
 |> fun x -> mk_and x (premiss_A ("S", "M"))
 |> fun x -> mk_imp x (premiss_A ("S", "P"))
 |> anglicize_syllogism

Example

 !!"P(x)"
 |> anglicize_syllogism

Constructs an atom of the form p(x).

p : string

The input monadic predicate.

x : string

The input variable.

Returns: formula<fol>

The atom p(x).

Example

 atom "P" "x"

Constructs an A premiss (universal affirmative) 'all S are P' \(\forall x.\ S(x) \Rightarrow P(x)\).

p : string

The first input monadic predicate.

q : string

The second input monadic predicate.

Returns: formula<fol>

The formula forall x. p(x) ==> q(x).

Example

 premiss_A ("P", "S")

Constructs an E premiss (universal negative) 'no S are P' \(\forall x.\ S(x) \Rightarrow \lnot P(x)\).

p : string

The first input monadic predicate.

q : string

The second input monadic predicate.

Returns: formula<fol>

The formula forall x. p(x) ==> ~q(x).

Example

 premiss_E ("P", "S")

Constructs an I premiss (particular affirmative) 'some S are P' \(\exists x.\ S(x) \land P(x)\).

p : string

The first input monadic predicate.

q : string

The second input monadic predicate.

Returns: formula<fol>

The formula exists x. p(x) /\ q(x).

Example

 premiss_I ("P", "S")

Constructs an O premiss (particular negative) 'some S are not P' \(\exists x.\ S(x) \land \lnot P(x)\).

p : string

The first input monadic predicate.

q : string

The second input monadic predicate.

Returns: formula<fol>

The formula exists x. p(x) /\ ~q(x).

Example

 premiss_O ("P", "S")

Enumerates all ways to interpreting function symbols.

dom : ('a * 'b) list

The input list of function name-arity pairs.

ran : 'b -> 'c list

The list of all possible functions in the domain.

Returns: ('a -> 'c) list

All interpretations of the input function symbols, i.e. all mappings from the function symbols in dom to the domain functions in ran.

Example

 let dom = [1..3]
 
 let functionSymbols = [("g",2)]
 let functions = allfunctions [1..3]
 
 alldepmappings functionSymbols functions
 |> List.mapi (fun i f -> 
     i, 
     dom 
     |> alltuples 2
     |> List.map (fun args -> args,f "g" args))
 |> List.take 3

 val it: (int * (int list * int) list) list =
   [(0,
     [([1; 1], 1); ([1; 2], 1); ([1; 3], 1); ([2; 1], 1); ([2; 2], 1);
      ([2; 3], 1); ([3; 1], 1); ([3; 2], 1); ([3; 3], 1)]);
    (1,
     [([1; 1], 1); ([1; 2], 1); ([1; 3], 1); ([2; 1], 1); ([2; 2], 1);
      ([2; 3], 1); ([3; 1], 1); ([3; 2], 1); ([3; 3], 2)]);
    (2,
     [([1; 1], 1); ([1; 2], 1); ([1; 3], 1); ([2; 1], 1); ([2; 2], 1);
      ([2; 3], 1); ([3; 1], 1); ([3; 2], 1); ([3; 3], 3)])]

Generates of the functions of a given finite domain with a given arity.

dom : 'a list

The input domain.

n : int

The input arity.

Returns: ('a list -> 'a) list

All the functions from dom to dom with arity n.

Example

 let dom = [1..3]
 
 allfunctions dom 2
 |> List.mapi (fun i f -> 
     i, 
     dom 
     |> alltuples 2
     |> List.map (fun args -> args, f args)
 )
 |> List.take 3

 val it: (int * (int list * int) list) list =
   [(0,
     [([1; 1], 1); ([1; 2], 1); ([1; 3], 1); ([2; 1], 1); ([2; 2], 1);
      ([2; 3], 1); ([3; 1], 1); ([3; 2], 1); ([3; 3], 1)]);
    (1,
     [([1; 1], 1); ([1; 2], 1); ([1; 3], 1); ([2; 1], 1); ([2; 2], 1);
      ([2; 3], 1); ([3; 1], 1); ([3; 2], 1); ([3; 3], 2)]);
    (2,
     [([1; 1], 1); ([1; 2], 1); ([1; 3], 1); ([2; 1], 1); ([2; 2], 1);
      ([2; 3], 1); ([3; 1], 1); ([3; 2], 1); ([3; 3], 3)])]

Generates all possible functions out of a finite domain into a finite range.

dom : 'a list

The input domain.

ran : 'b list

The input range.

Returns: ('a -> 'b) list

All possible functions out of the domain dom into range ran, and undefined outside dom.

Example

 let dom,ran = [1..3],[1..3]
 
 allmappings dom ran
 |> List.mapi (fun i f -> i, dom |> List.map f)

 [(0, [1; 1; 1]); (1, [1; 1; 2]); (2, [1; 1; 3]); (3, [1; 2; 1]);
  (4, [1; 2; 2]); (5, [1; 2; 3]); (6, [1; 3; 1]); (7, [1; 3; 2]);
  (8, [1; 3; 3]); (9, [2; 1; 1]); (10, [2; 1; 2]); (11, [2; 1; 3]);
  (12, [2; 2; 1]); (13, [2; 2; 2]); (14, [2; 2; 3]); (15, [2; 3; 1]);
  (16, [2; 3; 2]); (17, [2; 3; 3]); (18, [3; 1; 1]); (19, [3; 1; 2]);
  (20, [3; 1; 3]); (21, [3; 2; 1]); (22, [3; 2; 2]); (23, [3; 2; 3]);
  (24, [3; 3; 1]); (25, [3; 3; 2]); (26, [3; 3; 3])]

Generates of the predicates of a given finite domain with a given arity.

dom : 'a list

The input domain.

n : int

The input arity.

Returns: ('a list -> bool) list

All the possibile predicates in dom with arity n.

Example

 let dom = [1..3]
 
 allpredicates dom 2
 |> List.mapi (fun i f -> 
     i, 
     dom 
     |> alltuples 2
     |> List.map (fun args -> args, f args)
 )
 |> List.take 3

 val it: (int * (int list * bool) list) list =
   [(0,
     [([1; 1], false); ([1; 2], false); ([1; 3], false); ([2; 1], false);
      ([2; 2], false); ([2; 3], false); ([3; 1], false); ([3; 2], false);
      ([3; 3], false)]);
    (1,
     [([1; 1], false); ([1; 2], false); ([1; 3], false); ([2; 1], false);
      ([2; 2], false); ([2; 3], false); ([3; 1], false); ([3; 2], false);
      ([3; 3], true)]);
    (2,
     [([1; 1], false); ([1; 2], false); ([1; 3], false); ([2; 1], false);
      ([2; 2], false); ([2; 3], false); ([3; 1], false); ([3; 2], true);
      ([3; 3], false)])]

Generates all tuples of a given size with members chosen from a given list.

n : int

The size of the resulting tuples.

l : 'a list

The input list.

Returns: 'a list list

All tuples of size n with members chosen from the list l.

Example

 [1;2;3;4;5;6;7]
 |> alltuples 3

 [[1; 1; 1]; [1; 1; 2]; [1; 1; 3]; [1; 1; 4]; [1; 1; 5]; [1; 1; 6]; [1; 1; 7];
  [1; 2; 1]; [1; 2; 2]; [1; 2; 3]; [1; 2; 4]; [1; 2; 5]; [1; 2; 6]; [1; 2; 7];
  [1; 3; 1]; [1; 3; 2]; [1; 3; 3]; [1; 3; 4]; [1; 3; 5]; [1; 3; 6]; [1; 3; 7];
  [1; 4; 1]; [1; 4; 2]; [1; 4; 3]; [1; 4; 4]; [1; 4; 5]; [1; 4; 6]; [1; 4; 7];
  [1; 5; 1]; [1; 5; 2]; [1; 5; 3]; [1; 5; 4]; [1; 5; 5]; [1; 5; 6]; [1; 5; 7];
  [1; 6; 1]; [1; 6; 2]; [1; 6; 3]; [1; 6; 4]; [1; 6; 5]; [1; 6; 6]; [1; 6; 7];
  [1; 7; 1]; [1; 7; 2]; [1; 7; 3]; [1; 7; 4]; [1; 7; 5]; [1; 7; 6]; [1; 7; 7];
  [2; 1; 1]; [2; 1; 2]; [2; 1; 3]; [2; 1; 4]; [2; 1; 5]; [2; 1; 6]; [2; 1; 7];
  [2; 2; 1]; [2; 2; 2]; [2; 2; 3]; [2; 2; 4]; [2; 2; 5]; [2; 2; 6]; [2; 2; 7];
  [2; 3; 1]; [2; 3; 2]; [2; 3; 3]; [2; 3; 4]; [2; 3; 5]; [2; 3; 6]; [2; 3; 7];
  [2; 4; 1]; [2; 4; 2]; [2; 4; 3]; [2; 4; 4]; [2; 4; 5]; [2; 4; 6]; [2; 4; 7];
  [2; 5; 1]; [2; 5; 2]; [2; 5; 3]; [2; 5; 4]; [2; 5; 5]; [2; 5; 6]; [2; 5; 7];
  [2; 6; 1]; [2; 6; 2]; [2; 6; 3]; [2; 6; 4]; [2; 6; 5]; [2; 6; 6]; [2; 6; 7];
  [2; 7; 1]; [2; 7; 2]; [2; 7; 3]; [2; 7; 4]; [2; 7; 5]; [2; 7; 6]; [2; 7; 7];
  [3; 1; 1]; [3; 1; 2]; ...]

Tests if a formula holds in all interpretations of size n.

n : int

The input size of the interpretation.

fm : formula<fol>

The input formula.

Returns: bool

true, if fm holds in all interpretations of size n.

Example

 !! @"(forall x y. R(x,y) \/ R(y,x)) ==> forall x. R(x,x)"
 |> decide_finite 2

Tests if a formula (with the finite model property) is valid or invalid.

fm : formula<fol>

The input formula.

Returns: bool

true, if the input formula is valid; otherwise, false.

Note

Termination is guaranteed only for formulas with the finite model property.

Example

 !! @"(forall x y. R(x,y) \/ R(y,x)) ==> forall x. R(x,x)"
 |> decide_fmp

Example

 !! @"(forall x y z. R(x,y) /\ R(y,z) ==> R(x,z)) ==> forall x. R(x,x)"
 |> decide_fmp

Example

 !! @"~((forall x. ~R(x,x)) /\
        (forall x. exists z. R(x,z)) /\
        (forall x y z. R(x,y) /\ R(y,z) ==> R(x,z)))"
 |> decide_fmp

Tests if a monadic formula without function symbols is valid or invalid testing only interpretations of size \(2^k\) where \(k\) is the number of monadic predicates in the formula.

fm : formula<fol>

The input monadic formula.

Returns: bool

true, if the input monadic formula is valid; otherwise, false.

Example

 !! @"((exists x. forall y. P(x) <=> P(y)) <=>
       ((exists x. Q(x)) <=> (forall y. Q(y)))) <=>
      ((exists x. forall y. Q(x) <=> Q(y)) <=>
       ((exists x. P(x)) <=> (forall y. P(y))))"
 |> decide_monadic

Tests the validity of a formula by negating it and splitting in subproblems to be refuted with the core MESON procedure with a fixed limit of rules application.

n : int

The limit of rules application.

fm : formula<fol>

The input formula.

Returns: (func<string, term> * int * int) list

The list of triples with current instantiation, depth reached and number of variables renamed returned on the subproblems.

Example

 !! @"(forall x y. R(x,y) \/ R(y,x)) ==> forall x. R(x,x)"
 |> limited_meson 2
 |> List.map (fun (inst, n, k) -> (inst |> graph, n, k))

Tests the unsatisfiability of a formula using the core MESON procedure optimized with a fixed limit of rules application.

n : int

The limit of rules application.

fm : formula<fol>

The input formula.

Returns: func<string, term> * int * int

The triple with the current instantiation, the depth reached and the number of variables renamed.

Example

 !! @"~R(x,x) /\ (forall x y. R(x,y) \/ R(y,x))"
 |> limmeson 2
 |> fun (inst, n, k) -> (inst |> graph, n, k)