class Satre::Exists
Attributes
term[R]
variable[R]
Public Class Methods
new(variable, term)
click to toggle source
# File lib/satre/formula/first_order_logic/exists.rb, line 8 def initialize(variable, term) #fail(ArgumentError, '...') unless variable.is_a?(Formula) #fail(ArgumentError, '...') 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
Exists(x,p) -> exists (fun a -> holds m ((x |-> a) v) p) domain;;
# File lib/satre/formula/first_order_logic/exists.rb, line 21 def holds?(domain, func, pred, valudation) domain.any? 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/exists.rb, line 28 def to_s "∃ #{variable}. #{term}" end
wellformed?(sig)
click to toggle source
exists x. p is well-formed if p is well-formed
# File lib/satre/formula/first_order_logic/exists.rb, line 16 def wellformed?(sig) term.wellformed?(sig) end