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