TY - GEN

T1 - Combining deduction modulo and logics of fixed-point definitions

AU - Baelde, David

AU - Nadathur, Gopalan

PY - 2012

Y1 - 2012

N2 - Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. Specifically, we describe a natural deduction calculus that adds a form of ''closed-world'' equality - -a key ingredient to supporting fixed-point definitions - -to deduction modulo, a framework for extending a logic with a rewriting layer operating on formulas. We show that our calculus enjoys strong normalizability when the rewrite system satisfies general properties and we demonstrate its usefulness in specifying and reasoning about syntax-based descriptions. Our integration of closed-world equality into deduction modulo is based on an elimination principle for this form of equality that, for the first time, allows us to require finiteness of proofs without sacrificing stability under reduction.

AB - Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. Specifically, we describe a natural deduction calculus that adds a form of ''closed-world'' equality - -a key ingredient to supporting fixed-point definitions - -to deduction modulo, a framework for extending a logic with a rewriting layer operating on formulas. We show that our calculus enjoys strong normalizability when the rewrite system satisfies general properties and we demonstrate its usefulness in specifying and reasoning about syntax-based descriptions. Our integration of closed-world equality into deduction modulo is based on an elimination principle for this form of equality that, for the first time, allows us to require finiteness of proofs without sacrificing stability under reduction.

KW - closed-world equality

KW - deduction modulo

KW - fixed-point and recursive definitions

KW - strong normalizability

UR - http://www.scopus.com/inward/record.url?scp=84867178209&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84867178209&partnerID=8YFLogxK

U2 - 10.1109/LICS.2012.22

DO - 10.1109/LICS.2012.22

M3 - Conference contribution

AN - SCOPUS:84867178209

SN - 9780769547695

T3 - Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

SP - 105

EP - 114

BT - Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

T2 - 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

Y2 - 25 June 2012 through 28 June 2012

ER -