class Satre::Forall
Attributes
term[R]
variable[R]
Public Class Methods
new(variable, term)
click to toggle source
# File lib/satre/formula/first_order_logic/forall.rb, line 8 def initialize(variable, term) #fail(ArgumentError, "Variable was #{variable.class}") unless variable.is_a?(Formula) #fail(ArgumentError, "Term was #{term.class}") unless term.is_a?(Formula) @variable = variable.dup.freeze @term = term.dup.freeze end
Public Instance Methods
holds?(domain, func, pred, valudation)
click to toggle source
| Forall(x,p) -> forall (fun a -> holds m ((x |-> a) v) p) domain
# File lib/satre/formula/first_order_logic/forall.rb, line 21 def holds?(domain, func, pred, valudation) domain.all? do |a| valudation[variable.to_s.to_sym] = a term.holds?(domain, func, pred, valudation) end end
to_s()
click to toggle source
# File lib/satre/formula/first_order_logic/forall.rb, line 28 def to_s "∀ #{variable}. #{term}" end
wellformed?(sig)
click to toggle source
forall x. p is well-formed if p is well-formed
# File lib/satre/formula/first_order_logic/forall.rb, line 16 def wellformed?(sig) term.wellformed?(sig) end