class Satre::Fol_Formula
Public Instance Methods
holds?(domain, func, predicate, valudation)
click to toggle source
let rec holds (domain, func, pred as m) v fm =
match fm with False -> false | True -> true | Atom(R(r,args)) -> pred r (map (termval m v) args) | Not(p) -> not(holds m v p) | And(p,q) -> (holds m v p) & (holds m v q) | Or(p,q) -> (holds m v p) or (holds m v q) | Imp(p,q) -> not(holds m v p) or (holds m v q) | Iff(p,q) -> (holds m v p = holds m v q) | Forall(x,p) -> forall (fun a -> holds m ((x |-> a) v) p) domain | Exists(x,p) -> exists (fun a -> holds m ((x |-> a) v) p) domani;;
# File lib/satre/formula/first_order_logic/fol_formula.rb, line 18 def holds?(domain, func, predicate, valudation) fail 'abstract method' end
wellformed?(signature)
click to toggle source
-
Predicate $p(x_1, dots, x_n)$ is well-formed if (a) Each term is $x_1, dots, x_n$ is well formed (b) There is a pair (q, m) in signature sig q = p and n = m
-
p //\ q is wellformed if p and q are wellformed
-
p // q is wellformed if p and q are wellformed
-
p ==> q is wellformed if p and q are wellformed
-
p <=> q is wellformed if p and q are wellformed
-
forall x. p and exists x. p are wellformed if p is wellformed
# File lib/satre/formula/first_order_logic/fol_formula.rb, line 31 def wellformed?(signature) fail 'abstract method' end