Combining logic programs and monadic second order logics by program transformation

DOI10.1007/3-540-45013-0_14MaRDI QIDQ3079918zbMATH OpenOpenAlexFDO

Authors Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

Publication date 4 March 2011

Published in Logic Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-45013-0_14

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Logic program synthesis from first-order logic specifications
• scientific article; zbMATH DE number 970703
• Synthesis and transformation of logic programs using unfold/fold proofs
• Synthesis of positive logic programs for checking a class of definitions with infinite quantification
• Transformations of logic programs on infinite lists

Cited in

(4)

• Deciding full branching time logic by program transformation
• Transformations of logic programs on infinite lists
• Combining WS1S and HOL
• Formalizing Dijkstra's predicate transformer wp in weak second-order logic

Describes a project that uses

Uses Software

• MONA

This page was built for publication: Combining logic programs and monadic second order logics by program transformation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3079918)