class ADSL::FOL::Equiv

Public Class Methods

new(*subformulae) click to toggle source
# File lib/adsl/fol/first_order_logic.rb, line 154
def initialize(*subformulae)
  @subformulae = subformulae.flatten
  raise ArgumentError, "At least two subformulae required" if @subformulae.length < 2
end

Public Instance Methods

resolve_spass() click to toggle source
# File lib/adsl/fol/first_order_logic.rb, line 159
def resolve_spass
  subformulae = @subformulae.map{ |sub| sub.resolve_spass }
  return subformulae.first if subformulae.length == 1
  return And.new(subformulae).resolve_spass if subformulae.include? 'true'
  return Not.new(subformulae).resolve_spass if subformulae.include? 'false'
  combinations = []
  (subformulae.length-1).times do |index|
    combinations << "equiv(#{subformulae[index]}, #{subformulae[index+1]})"
  end
  return And.new(combinations).resolve_spass
end