Resource Graphs and Countermodels in Resource Logics |
| |
Authors: | Didier Galmiche,Daniel M ry |
| |
Affiliation: | LORIA UMR 7503 - Université Henri Poincaré, Campus Scientifique, BP 239, 54506 Vandœuvre-les-Nancy, France |
| |
Abstract: | In this abstract we emphasize the role of a semantic structure called resource graph in order to study the provability in some resource-sensitive logics, like the Bunched Implications Logic (BI) or the Non-commutative Logic (NL). Such a semantic structure is appropriate for capturing the particular interactions between different kinds of connectives (additives and multiplicatives in BI, commutatives and non-commutatives in NL) that occur during proof-search and is also well-suited for providing countermodels in case of non-provability. We illustrate the key points with a tableau method with labels and constraints for BI and then present tools, namely BILL and CheckBI, which are respectively dedicated to countermodel generation and verification in this logic. |
| |
Keywords: | resources proof-search semantics labels countermodels |
本文献已被 ScienceDirect 等数据库收录! |
|