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