Serge Autexier
In this talk we present a framework which provides a set of basic uniform reasoning rules, which provide a logic-independent basis to define generic tactics. The reasoning rules capture the essence of window inference reasoning and encapsulate any logical specificities. The soundness with respect to a variety of logics is ensured inside the framework by a uniform mechanism extending techniques developed by Wallen on the basis of position trees in the context of matrix characterizations. A unified notation for windows and position trees is developed and the basic reasoning rules of the framework are defined on the unified notation. The soundness with respect to a variety of logics of the reasoning rules of the framework is proved using the unified notation and the techniques developed by Wallen.