Class: ADSL::FOL::OneOf

Inherits:
Object show all
Defined in:
lib/adsl/fol/first_order_logic.rb

Instance Method Summary collapse

Constructor Details

#initialize(*formulae) ⇒ OneOf

Returns a new instance of OneOf.



190
191
192
 
# File 'lib/adsl/fol/first_order_logic.rb', line 190

def initialize(*formulae)
  @formulae = formulae.flatten
end

Instance Method Details

#resolve_spass ⇒ Object 



194
195
196
197
198
199
200
201
202
203
204
205
 
# 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