Perfect Model Checking via Unfold/Fold Transformations

1. K. R. Apt and R. N. Bol. Logic programming and negation: A survey. Journal of Logic Programming, 19,20:9–71, 1994.

   Article  MathSciNet  Google Scholar 

2. R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, New York, 1979.

   MATH  Google Scholar 

3. S. Brass and J. Dix. Semantics of (disjunctive) logic programs based on partial evaluation. Journal of Logic Programming, 40:1–46, 1999.

   Article  MATH  MathSciNet  Google Scholar 

4. R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. JACM, 24(1):44–67, January 1977.

   Google Scholar 

5. W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. JACM, 43(1), 1996.

   Google Scholar 

6. K. L. Clark. Negation as failure. In H. Gallaire and J. Minker (eds.) Logic and Data Bases, 293–322. Plenum Press, New York, 1978.

   Google Scholar 

7. H. Comon and R. Nieuwenhuis. Induction = I-axiomatization + first-order consistency. Information and Computation. (To appear).

   Google Scholar 

8. B. Courcelle. Equivalences and Transformations of Regular Systems-Applications to Recursive Program Schemes and Grammars. Theo. Comp. Sci., 42:1–122, 1986.

   Article  MATH  MathSciNet  Google Scholar 

9. E. A. Emerson. Temporal and modal logic. In J. van Leuveen (ed.) Handbook of Theoretical Computer Science, volume B, 997–1072. Elsevier, 1990.

   Google Scholar 

10. J. Engelfriet. Tree Automata and Tree Grammars. DAIMI FN-10, Department of Computer Science, University of Aarhus, Denmark, April 1975.

    Google Scholar 

11. L. Kott. Unfold/fold program transformation. In M. Nivat and J.C. Reynolds (eds.) Algebraic Methods in Semantics, 411–434. Cambridge University Press, 1985.

    Google Scholar 

12. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987. 2nd Ed.

    Google Scholar 

13. A. Pettorossi and M. Proietti. Synthesis and transformation of logic programs using unfold/fold proofs. Journal of Logic Programming, 41(2&3):197–230, 1999.

    Article  MATH  MathSciNet  Google Scholar 

14. M. Proietti and A. Pettorossi. Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theo. Comp. Sci., 142(1):89–124, 1995.

    Article  MATH  MathSciNet  Google Scholar 

15. T. C. Przymusinski. On the declarative and procedural semantics of logic programs. Journal of Automated Reasoning, 5:167–205, 1989.

    Article  MATH  MathSciNet  Google Scholar 

16. M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–34, July 1969.

    Google Scholar 

17. A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan, and S. A. Smolka. Verification of parametrized systems using logic program transformations. In Proc. TACAS 2000, LNCS 1785, 172–187. Springer, 2000.

    Google Scholar 

18. Y.S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proc. CAV’ 97, LNCS 1254, 143–154. Springer, 1997.

    Google Scholar 

19. H. Seki. Unfold/fold transformation of stratified programs. Theo. Comp. Sci., 86:107–139, 1991.

    Article  MATH  MathSciNet  Google Scholar 

20. H. Tamaki and T. Sato. Unfold/fold transformation of logic programs. In Proceedings of ICLP’84, 127–138. Uppsala University, Sweden, 1984.

    Google Scholar 

Download references