""" Propositional rules used in all sources: Kaye, Huth&Ryan, and Bornat Supplement this module with more rules from prop_classic (Kaye), prop_derived (H&R), or prop_constructive (Bornat) Rules here based on Kaye ch 6, defn. 6.3, p. 65, impl. from defn. 6.22, p. 76 See also Bornat, table 3.10, p. 43 and Huth&Ryan, Fig. 1.2, p. 27 """ from formula import Letter, PrefixLogical, InfixLogical, FormulaPlaceholder # T, F are just propositional letters that appear in inference rules T,F = map(Letter, 'TF') class Not(PrefixLogical): """ Not(a) means ~a in Kaye. Capitalize Not to distinguish from Python keyword """ def __init__(self, *args): PrefixLogical.__init__(self, *args) self.symbol = '~' class And(InfixLogical): """ And(a,b) means a & b in Kaye. Capitalize And, distinguish from Python keyword """ def __init__(self, *args): InfixLogical.__init__(self, *args) self.symbol = '&' class Or(InfixLogical): """ Or(a,b) means a v b in Kaye. Capitalize Or, distinguish from Python keyword """ def __init__(self, *args): InfixLogical.__init__(self, *args) self.symbol = 'v' class Impl(InfixLogical): """ Impl(a,b) means a -> b in Kaye """ def __init__(self, *args): InfixLogical.__init__(self, *args) self.symbol = '->' # Define symbol for each rule, short for easy typing at Python interpreter # Rule symbols are self-evaluating, used to write proof in save file format # Rules for core propositional logic from Kaye # Use Kaye's nomenclature: raa and contra are Bornat's not-intro and not-elim. # All the rules here are constructive so they can be used with Bornat. # Kaye's Not-elim (double negation elim) is not included, it's not constructive # Or-elim is not included here; Kaye uses different forms than Bornat or H&R assume, top, ai, ael, aer, oil, oir, contra, raa, impli, imple = \ 'assume','top','ai','ael','aer','oil','oir','contra','raa','impli','imple' # Pretty-print names for rules. # Each logic module merges its own rule_names with checker.rule_names # Note _ prefix on _rule_names here makes it private _rule_names = { assume: 'Assumption', top: 'Top rule', ai: 'And-Introduction', ael: 'And-Elimination (Left)', aer: 'And-Elimination (Right)', oil: 'Or-Introduction (Left)', oir: 'Or-Introduction (Right)', contra : 'Contradiction', raa: 'Reductio Ad Absurdum', impli: 'Implication-Introduction', imple: 'Implication-Elimination (Modus Ponens)' } # Inference rules, dictionary of rule symbol and list of formulas: # list of premises, then conclusion last # Subproofs in inference rules are nested lists # Placeholders used in rules m1, m2 = map(FormulaPlaceholder, ('m1','m2')) _rules = { assume: [[ m1 ]], # subproof, assumer top: [ T ], ai: [ m1, m2, And(m1,m2) ], ael: [ And(m1,m2), m2 ], aer: [ And(m1,m2), m1 ], oil: [ m2, Or(m1,m2) ], oir: [ m1, Or(m1,m2) ], contra: [ m1, Not(m1), F ], raa: [[ m1, F ], Not(m1) ], # subproof, discharger impli: [[ m1, m2], Impl(m1,m2) ], # ditto imple: [ Impl(m1,m2), m1, m2 ] } # Propositional letters used in proofs # Use a,b,p,t for Kaye's alpha, beta, psi, theta a,b,c,d,e,f,p,q,r,t = map(Letter, 'abcdefpqrt') # a.name = 'a' etc. # Import statement to write to save file, so it in turn can be imported _imports = 'from flip.logic.prop_common import *'