Unsorted Functional Translations

Areces, C. and Gorín, D. Unsorted Functional Translations. Electronic Notes in Theoretical Computer Science, 278(0):3–16, 2011. Proceedings of the 7th Workshop on Methods for Modalities (M4M 2011)

Download: [pdf] 

Abstract:

In this article we first show how the functional and the optimized functional translation from modal logic to many-sorted first-order logic can be naturally extended to the hybrid language H(@,\downarrow). The translation is correct not only when reasoning over the class of all models, but for any first-order definable class. We then show that sorts can be safely removed (i.e., without affecting the satisfiability status of the formula) for frame classes that can be defined in the basic modal language, and show a counterexample for a frame class defined using nominals.

BibTeX: (download)

@ARTICLE{arec:unso11,
  author = {Areces, C. and Gor\'{\i}n, D},
  title = {Unsorted Functional Translations},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = {2011},
  volume = {278},
  pages = {3-16},
  number = {0},
  note = {Proceedings of the 7th Workshop on Methods for Modalities (M4M 2011)},
  abstract = {In this article we first show how the functional and the optimized
	functional translation from modal logic to many-sorted first-order
	logic can be naturally extended to the hybrid language H(@,\downarrow).
	The translation is correct not only when reasoning over the class
	of all models, but for any first-order definable class. We then show
	that sorts can be safely removed (i.e., without affecting the satisfiability
	status of the formula) for frame classes that can be defined in the
	basic modal language, and show a counterexample for a frame class
	defined using nominals.},
  doi = {10.1016/j.entcs.2011.10.002},
  issn = {1571-0661},
  keywords = {Automated theorem proving},
  url = {http://www.sciencedirect.com/science/article/pii/S1571066111001307}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49