Parse/Evaluate Symbolic Logic

-=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- (c) WidthPadding Industries 1987 0\|40\|0 -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=- -=+=-
SoCoder -> Snippet Home -> Misc

Cower	Created : 21 September 2009 Edited : 12 March 2014 Language : Ruby Parse/Evaluate Symbolic Logic Also generates truth tables (doesn't handle proofs)
Alrighty, re-added this. logical.rb #!/usr/bin/env ruby -w # Copyright (c) 2009 Noel R. Cower # # Permission is hereby granted, free of charge, to any person obtaining a copy # of this software and associated documentation files (the "Software"), to deal # in the Software without restriction, including without limitation the rights # to use, copy, modify, merge, publish, distribute, sublicense, and/or sell # copies of the Software, and to permit persons to whom the Software is # furnished to do so, subject to the following conditions: # # The above copyright notice and this permission notice shall be included in # all copies or substantial portions of the Software. # # THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR # IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, # FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE # AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER # LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN # THE SOFTWARE. class Argument attr_reader :premises, :conclusion attr_reader :symbols, :table def rebuild_symbols @symbols = [@conclusion, @premises].inject([]) { \|m,e\| m+e.symbols }.uniq.sort {\|a,b\|a.to_s<=>b.to_s}.freeze @table = table_for_symbols(@symbols).freeze end private :rebuild_symbols def premises=(ps) if ps.kind_of?(String) then @premises = ps.split(',').inject([]) { \|m,e\| m << expression(e) } elsif ps.respond_to? :to_ary then @premises = ps.to_ary.collect {\|i\| i.kind_of?(LogicOperator) ? i : expression(i)}.freeze else raise ArgumentError, "Invalid type of object for premises" end rebuild_symbols end def conclusion=(cn) @conclusion = expression(cn) rebuild_symbols end def invalid? # i = invalids list, t = table, l = last/memo (true/false), p = premise # Iterate over the lookup tables, and if the argument is invalid with that lookup table (evaluation: all premises true and conclusion false), then insert that table into the invalids list # return (invalids = self.table.inject([]) { \|i,t\| (( not @conclusion.eval(t) and @premises.inject(true) { \|l, p\| l and p.eval(t) } ) ? i << t : i) }).empty? ? nil : invalids return self.table.inject(nil) { \|memo, table\| premises_true = @premises.inject(true) { \|last, premise\| last and premise.eval(table) } if @conclusion.eval(table) and premises_true then if memo.nil? then # create list with table [table] else # add table to list memo << table end else #nop memo end } end def sound? return false if invalid? self.table.each do \|table\| if @conclusion.eval(table) and @premises.inject(true) { \|last, premise\| last and premise.eval(table) } then return true end end return false end def initialize(argument) if argument.kind_of? String then matchdata = argument.match(/^(.+):\.(.+)$/) raise "Invalid argument: no conclusion found" unless matchdata @premises = matchdata[1].split(',').inject([]) { \|m,e\| m << expression(e) } @conclusion = expression(matchdata[2]) rebuild_symbols else raise "Invalid argument: not a string" end end def to_s "#{@premises.join(', ')} :. #{@conclusion}" end def truthtable(table=nil) if table then if table.kind_of?(Hash) then table = [table] end else table = @table end tablestring = string_for_table(table).split("\n").collect {\|i\| "#{i}\|"} exprstring = to_s tablestring[0] += " #{exprstring}" tablestring[1] += '-'(exprstring.length+1) (2..tablestring.length-1).each do \|i\| tablestring[i] += "#{@premises.inject('') {\|m, e\| "#{m} #{e.with_table_values(table[i-2])}"}} #{@conclusion.with_table_values(table[i-2])}".reverse.chomp(' ').reverse end return tablestring.join("\n") end end class LogicOperator def initialize end def to_s(root=true) raise "Not implemented" end def eval(table) raise "Not implemented" if self.class === LogicOperator raise "No lookup table provided for operands" if table.nil? or not table.respond_to?(:fetch) end def with_table_values(table, root=true) raise "Not implemented" end def when(truthiness) return table_for_expression(self).select do \|table\| eval(table)==truthiness end end def symbols list = [] if respond_to?(:operand) then if self.kind_of?(Atom) then list << @operand else list += @operand.symbols end elsif respond_to?(:left) and respond_to?(:right) then list += @left.symbols + @right.symbols else raise "Invalid operator implementation" end list.sort! {\|a,b\|a.to_s<=>b.to_s}.uniq! return list end def tautology? table_for_expression(self).each { \|t\| return false unless eval(t) } return true end def truthtable table = table_for_expression(self) tablestring = string_for_table(table).split("\n").collect {\|i\| "#{i}\|"} exprstring = to_s tablestring[0] += " #{exprstring} " tablestring[1] += "-"(exprstring.length+3) (2..tablestring.length-1).each do \|i\| tablestring[i] += " #{with_table_values(table[i-2])} " end return tablestring.join("\n") end end class Atom < LogicOperator attr_accessor :operand def initialize(op) @operand = op end def with_table_values(table, root=true) root ? (eval(table) ? 'T' : 'F') : ' ' end def eval(table) super(table) raise "Nil operand" if @operand.nil? table.fetch(@operand) do \|op\| raise "No value for operand '#{op.to_s}'" end end def to_s(root=true) return @operand.to_s end end class Negation < LogicOperator attr_accessor :operand def initialize(op) @operand = op end def eval(table) super table raise "Nil operand" if @operand.nil? !@operand.eval(table) end def with_table_values(table) "#{eval(table) ? 'T' : 'F'}#{@operand.with_table_values(table, false)}" end def to_s(root=true) return "~#{@operand.to_s(false)}" end end class Disjunction < LogicOperator attr_accessor :left, :right def initialize(left, right) @left = left @right = right end def eval(table) super table raise "Invalid operand(s)" unless @left.kind_of?(LogicOperator) or @right.kind_of?(LogicOperator) @left.eval(table) or @right.eval(table) end def with_table_values(table, root=true) r="#{@left.with_table_values(table, false)} #{eval(table) ? 'T' : 'F'} #{@right.with_table_values(table, false)}" root ? r : " #{r} " end def to_s(root=true) r="#{@left.to_s(false)} v #{@right.to_s(false)}" root ? r : "(#{r})" end end class Conjunction < LogicOperator attr_accessor :left, :right def initialize(left, right) @left = left @right = right end def eval(table) super table raise "Invalid operand(s)" unless @left.kind_of?(LogicOperator) or @right.kind_of?(LogicOperator) @left.eval(table) and @right.eval(table) end def with_table_values(table, root=true) r="#{@left.with_table_values(table, false)} #{eval(table) ? 'T' : 'F'} #{@right.with_table_values(table, false)}" root ? r : " #{r} " end def to_s(root=true) r="#{@left.to_s(false)} . #{@right.to_s(false)}" root ? r : "(#{r})" end end class Conditional < LogicOperator attr_accessor :left, :right def initialize(left, right) @left = left @right = right end def eval(table) super table raise "Invalid operand(s)" unless @left.kind_of?(LogicOperator) or @right.kind_of?(LogicOperator) !(@left.eval(table) and !@right.eval(table)) end def with_table_values(table, root=true) r="#{@left.with_table_values(table, false)} #{eval(table) ? 'T' : 'F'} #{@right.with_table_values(table, false)}" root ? r : " #{r} " end def to_s(root=true) r="#{@left.to_s(false)} -> #{@right.to_s(false)}" root ? r : "(#{r})" end end class Biconditional < LogicOperator attr_accessor :left, :right def initialize(left, right) @left = left @right = right end def eval(table) super table raise "Invalid operand(s)" unless @left.kind_of?(LogicOperator) or @right.kind_of?(LogicOperator) @left.eval(table) == @right.eval(table) end def with_table_values(table, root=true) r="#{@left.with_table_values(table, false)} #{eval(table) ? 'T' : 'F'} #{@right.with_table_values(table, false)}" root ? r : " #{r} " end def to_s(root=true) r="#{@left.to_s(false)} <-> #{@right.to_s(false)}" root ? r : "(#{r})" end end def table_for_symbols(syms) syms = syms.sort {\|a,b\|a.to_s<=>b.to_s} num_lookups = 2syms.length table = Array.new(syms.length) {Array.new(num_lookups, true)} table.each_with_index do \|item, index\| skip = 2(table.length-(index+1)) index = skip while index < item.length do item[range = (index..index+skip-1)] = Array.new(range.count, false) index += skip2 end end Array.new(num_lookups) do \|index\| item = {} syms.each_with_index { \|sym, sid\| item[sym] = table[sid][index] } item end end def __tfr_r(s, symbols) if s.kind_of?(Atom) then symbols << s.operand elsif s.kind_of?(Negation) then __tfr_r(s.operand, symbols) else __tfr_r(s.left, symbols) __tfr_r(s.right, symbols) end end def table_for_expression(expr) symbols = [] __tfr_r expr, symbols symbols.uniq! return table_for_symbols(symbols) end def string_for_table(table) syms = table[0].keys.sort {\|a,b\|a.to_s<=>b.to_s} length = 2syms.length "#{syms.join(' ')} \n#{'-'length}\n#{ Array.new(2*syms.length) do \|index\| "#{Array.new(syms.length) do \|vid\| table[index][syms[vid]] ? 'T' : 'F' end.join(' ')} " end.join($/)}" end def compile_rec(block) return block if block.kind_of?(Atom) left = compile_rec(block[:left]) right = compile_rec(block[:right]) if block[:right] left = Negation.new(left) if block[:negate_left] right = Negation.new(right) if block[:negate_right] compiled = case block[:op] when :conjunction Conjunction.new(left, right) when :disjunction Disjunction.new(left, right) when :conditional Conditional.new(left, right) when :biconditional Biconditional.new(left, right) else left end return compiled end # assumes expr is a WFF (with permissible departures) def expression(expr) expr = expr.gsub(/[\[\].v]\|<?->\|~/) {" #{$&} "}.gsub(/\s{2,}/, ' ').split top = {:negate_left=>false, :negate_right=>false, :upper=>nil, :op=>nil} expr.each do \|token\| side = top[:left].nil? ? :left : :right case token when '(','[' then top = top[side] = {:upper => top, :negate_left=>false, :negate_right=>false} when ')',']' then raise "Expression is not a WFF" unless top[:upper] top = top[:upper] when '~' then top[top[:left].nil? ? :negate_left : :negate_right] = !top[top[:left].nil? ? :negate_left : :negate_right] when 'v' then raise "Expression is not a WFF" if top[:op] top[:op] = :disjunction when '.' then raise "Expression is not a WFF" if top[:op] top[:op] = :conjunction when '->' raise "Expression is not a WFF" if top[:op] top[:op] = :conditional when '<->' raise "Expression is not a WFF" if top[:op] top[:op] = :biconditional else raise "Invalid atomic statement: #{token}" unless /^[A-Z]$/ === token top[side] = Atom.new(token.to_sym) # assume atomic statement end end raise "Expression is not a WFF" if top[:upper] return compile_rec(top) end --v Example: #!/usr/bin/env ruby19 -w require 'logical.rb' arg = Argument.new("A v B, ~B :. A") expr = expression("A->~B") puts arg.invalid? ? 'invalid' : 'valid' puts arg.to_s puts arg.sound? ? 'sound' : 'unsound' puts arg.truthtable --v Note: this is set to run using Ruby 1.9.1 on my machine. You do not need Ruby 1.9, it will work with 1.8.7 (and probably 1.8.6 as well).* Jay, fix the Language/System thingy please >_>

Comments
Monday, 21 September 2009, 09:18
Jayenkai	My head doesn't scan through stuff like that as well as it does standard "a=b+c" stuff. I tend to need to closely read it before I can understand what my code's doing, so I tend to stay away from "complex" looking stuff like that. I'm sure it's useful, though!
Monday, 21 September 2009, 10:41
Cower	Ruby isn't really that complex. It just tends to look that way since there are a few things that other languages don't have (since most languages are not near as flexible when it comes to syntax). Anyhow, updated it so that there's a bug fixed with incorrectly parsing WFFs, moved the tautology? method into the LogicOperator method (it really has no business being in here at all, but I like it), and added some methods to determine when an expression is true/false and to return a string with a complete truth table for the expression.
Friday, 25 September 2009, 22:26
Cower	I've taken this down for the time being.
Saturday, 26 September 2009, 02:46
Jayenkai	How come?
Saturday, 26 September 2009, 03:36
JL235	Why take it down? It's really nice to see some non-gaming code snippets, especially those done in Ruby and written to a high standard. It would be nice to see this re-added.
Saturday, 26 September 2009, 20:16
Cower	There is the possibility for the university to disagree with my intent in writing the code, so for the time being, it's gone.
Thursday, 01 October 2009, 19:37
Cower	Re-added this since there's unlikely to be any disagreement now.

Parse/Evaluate Symbolic Logic

Comments