class ADSL::FOL::OneOf

Public Class Methods

new(*formulae) click to toggle source
# File lib/adsl/fol/first_order_logic.rb, line 190
def initialize(*formulae)
  @formulae = formulae.flatten
end

Public Instance Methods

resolve_spass() click to toggle source
# File lib/adsl/fol/first_order_logic.rb, line 194
def resolve_spass
  return 'false' if @formulae.empty?
  return @formulae.first.resolve_spass if @formulae.length == 1
  return Equiv.new(Not.new(@formulae.first), @formulae.last).resolve_spass if @formulae.length == 2

  substatements = []
  @formulae.length.times do |i|
    formulae_without_i = @formulae.first(i) + @formulae.last(@formulae.length - 1 - i)
    substatements << Implies.new(@formulae[i], Not.new(formulae_without_i))
  end
  And.new(Or.new(@formulae), substatements).resolve_spass
end