Class: ADSL::FOL::Equiv

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

Instance Method Summary collapse

Constructor Details

#initialize(*subformulae) ⇒ Equiv

Returns a new instance of Equiv.

Raises:

  • (ArgumentError) 


154
155
156
157
 
# 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

Instance Method Details

#resolve_spass ⇒ Object 



159
160
161
162
163
164
165
166
167
168
169
 
# 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