New insights on the intuitionistic interpretation of Default Logic
Pedro Cabalar, David Lorenzo · 2004
An interesting result found by Truszczynski showed that (non-monotonic) modal logic S4F can be used to encode Default Logic (DL). In this work we further investigate the relation between both formalisms using Godel's pattern for translation of Intuitionistic Logic into S4. This pattern not only allows encoding DL into S4F but also preserves this feature for two general nonmonotonic formalisms: Turner's Nested Default Logic (NDL) and Pearce's Equilibrium Logic (which encodes logic programs into the intermediate logic of Here-and-There). For comparison purposes, we define a variation of DL (inside S4F) we have called Intuitionistic Default Logic that generalizes both NDL and Equilibrium Logic, in the sense that the former does not allow nesting or combining the rule conditional operator, whereas the latter exclusively restricts the shape of classical formulas to atoms. Finally, we also prove that the S4F-equivalence of the modal encodings is a necessary and su#cient condition for strong equivalence of IDL default theories.