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