Deciding theoremhood in fibred logics without shared connectives

Sergio Marcelino

Carlos Caleiro

Pedro Baltazar

pp. 387-406

in: Arnold Koslow, Arthur Buchsbaum (eds), The road to universal logic II, Basel, Birkhäuser, 2015

Abstract

Fibring is a powerful mechanism for combining logics, and an essential tool for designing and understanding complex logical systems. Abstract results about the semantics and proof theory of fibered logics have been extensively developed, including general soundness and completeness preservation results. Decidability, however, a key ingredient for the automated support of the fibered logic, has not deserved similar attention.In this chapter, we address the problem of deciding theoremhood in fibered logics without shared connectives. Namely, under this assumption, we provide a full characterization of the mixed patterns of reasoning that leads to theorems in the fibered logic, and uses it to prove a general decidability preservation result. The complexity of the decision procedure we obtain is also analyzed.