Reasoning on Schemata of Formulæ

1. Aczel, P.: An Introduction to Inductive Definitions. In: Barwise, K.J. (ed.) Handbook of Mathematical Logic, pp. 739–782. North-Holland, Amsterdam (1977)

   Chapter  Google Scholar 

2. Aravantinos, V., Caferra, R., Peltier, N.: A Schemata Calculus for Propositional Logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 32–46. Springer, Heidelberg (2009)

   Chapter  Google Scholar 

3. Aravantinos, V., Caferra, R., Peltier, N.: Decidability and undecidability results for propositional schemata. Journal of Artificial Intelligence Research 40, 599–656 (2011)

   MathSciNet  MATH  Google Scholar 

4. Aravantinos, V., Peltier, N.: Schemata of SMT-Problems. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 27–42. Springer, Heidelberg (2011)

   Chapter  Google Scholar 

5. Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Theor. Comput. Sci. 403(2-3), 160–175 (2008)

   Article  MathSciNet  MATH  Google Scholar 

6. Baelde, D., Miller, D., Snow, Z.: Focused Inductive Theorem Proving. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 278–292. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

7. Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

8. Bouhoula, A., Kounalis, E., Rusinowitch, M.: SPIKE, an Automatic Theorem Prover. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 460–462. Springer, Heidelberg (1992)

   Chapter  Google Scholar 

9. Bouhoula, A., Rusinowitch, M.: Implicit induction in conditional theories. Journal of Automated Reasoning 14, 14–189 (1995)

   Article  MathSciNet  Google Scholar 

10. Boyer, R.S., Moore, J.S.: A Theorem Prover for a Computational Logic. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 1–15. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

11. Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 845–911. Elsevier and MIT Press (2001)

    Google Scholar 

12. Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 14, pp. 913–962. North-Holland (2001)

    Google Scholar 

13. Echenim, M., Peltier, N.: Reasoning on Schemata of Formulae. Technical report, CoRR, abs/1204.2990 (2012)

    Google Scholar 

14. Giesl, J., Kapur, D.: Decidable Classes of Inductive Theorems. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 469–484. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

15. Gupta, A., Fisher, A.L.: Parametric Circuit Representation Using Inductive Boolean Functions. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 15–28. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

16. Kapur, D., Musser, D.: Proof by consistency. Artificial Intelligence 31 (1987)

    Google Scholar 

17. Lenzi, G.: A New Logical Characterization of Büchi Automata. In: Ferreira, A., Reichel, H. (eds.) STACS 2001. LNCS, vol. 2010, pp. 467–477. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

18. Park, D.M.: Finiteness is Mu-ineffable. Theoretical Computer Science 3, 173–181 (1976)

    Article  MathSciNet  Google Scholar 

19. Paulin-Mohring, C.: Inductive Definitions in the system Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

Download references