class Satre::Relation

A first-order-logig relation between terms

Typical relations are

p > q - term p is greater than term p
p < q - term p is less than term p
p = q - term p is equvivalent to term p
p >= q - term p is greter or equvivalent to term q
p <= q - term p is less or equvivalent to term q
p != q - term p is not equvivalent to term q

Attributes

relation[R]
term_list[R]

Public Class Methods

new(relation, term_list) click to toggle source
# File lib/satre/formula/first_order_logic/relation.rb, line 17
def initialize(relation, term_list)
  @relation = relation.dup.freeze
  @term_list = term_list.dup.freeze
end

Public Instance Methods

holds?(domain, func, predicate, valudation) click to toggle source
# File lib/satre/formula/first_order_logic/relation.rb, line 22
def holds?(domain, func, predicate, valudation)
  predicate.call(relation, term_list.map { |t| t.validate(func, predicate, valudation) })
end
to_s() click to toggle source
# File lib/satre/formula/first_order_logic/relation.rb, line 32
def to_s
  return term_list.map(&:to_s).join(relation.to_s) if ['>','<','=','<=','>=','!='].include?(relation)
  s = term_list.map(&:to_s).join(',')
  "#{relation}#{"("+s+")" unless s.to_s == ''}"
end
wellformed?(sig) click to toggle source

A predicate p(x_1,…,x_n) is well-formed if

(a) each term x_1,...,x_n is well-formed
(b) there is a pair (q, m) in signature sig where q = p and n = m
# File lib/satre/formula/first_order_logic/relation.rb, line 28
def wellformed?(sig)
  term_list.all? { |x| x.wellformed?(sig) } && sig[relation.to_sym] == term_list.length
end