Combining Logic Programs and Monadic Second Order Logics by Program Transformation

Simple item page
dc.creatorFioravanti, F.
dc.creatorPettorossi, A.
dc.creatorProietti, M.
dc.date2003-11-27
dc.date.accessioned2026-07-07T03:20:38Z
dc.date.available2026-07-07T03:20:38Z
dc.descriptionWe present a program synthesis method based on unfold/fold transformation rules which can be used for deriving terminating definite logic programs from formulas of the Weak Monadic Second Order theory of one successor (WS1S). This synthesis method can also be used as a proof method which is a decision procedure for closed formulas of WS1S. We apply our synthesis method for translating CLP(WS1S) programs into logic programs and we use it also as a proof method for verifying safety properties of infinite state systems.
dc.description25 pages. Full version of a paper that appears in: M. Leuschel (ed.) Proceedings of LOPSTR'02, Twelfth International Workshop on Logic-based Program Development and Transformation, Madrid, Spain, 17-20 Sept. 2002. Lecture Notes in Computer Science 2664. Springer-Verlag Berlin Heidelberg, 2003, pp. 160-181
dc.identifierhttps://arxiv.org/abs/cs/0311043
dc.identifierhttp://arxiv.org/abs/cs/0311043
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/31895
dc.subjectProgramming Languages
dc.subjectLogic in Computer Science
dc.subjectD.1.2;D.1.6;I.2.2;F.3.1
dc.titleCombining Logic Programs and Monadic Second Order Logics by Program Transformation
dc.typetext

Files

Collections

arXiv