On the Mechanization of the Proof of Hessenberg’s Theorem in Coherent Logic

1. Bezem, M., Coquand, T.: Newman’s lemma—a case study in proof automation and geometric logic. In: Păun, G., Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science, vol. 2, pp. 267–282. World Scientific, Singapore (2004)

   Google Scholar 

2. Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) Proceedings LPAR-12. Lecture Notes in Computer Science, vol. 3825, pp. 246–260. Springer-Verlag, Berlin (2005)

   Google Scholar 

3. Bezem, M., Hendriks, D.: Web page including CL tool, input files, Coq files. http://www.cs.vu.nl/~diem/research/ht/.

4. Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. J. Autom. Reason. 29(3), 253–275 (2002)

   Article  MATH  Google Scholar 

5. Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) Proceedings LPAR-14. Lecture Notes in Computer Science, vol. 4790, pp. 151–165. Springer-Verlag, Berlin (2007)

   Google Scholar 

6. Coxeter, H.S.M.: The Real Projective Plane, 2nd edn. Cambridge University Press, Cambridge (1955)

   MATH  Google Scholar 

7. Cronheim, A.: A proof of Hessenberg’s theorem. Proc. AMS 4(2), 219–221 (1953)

   Article  MATH  MathSciNet  Google Scholar 

8. de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199(1), 24–54 (2005) [Special Issue on the 19th International Conference on Automated Deduction (CADE-19)]

   Article  MATH  Google Scholar 

9. de Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: Harrison, J., Furbach, U., Shankar, N. (eds.) International Joint Conference on Automated Reasoning 2006, p. 15. Springer, Seattle (2006)

   Google Scholar 

10. Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM, 40(1), 143–184 (1993)

    Article  MATH  MathSciNet  Google Scholar 

11. Hessenberg, G.: Beweis des Desarguesschen Satzes aus dem Pascalschen. Math. Ann. 61, 161–172 (1905)

    Article  MathSciNet  Google Scholar 

12. Johnstone, P.: Sketches of an Elephant: A Topos Theory Compendium, vol. 2. Oxford University Press, London (2002)

    Google Scholar 

13. Kusak, E., Leończuk, W.: Hessenberg theorem. Formaliz. Math. 2(2), 217–219 (1991)

    Google Scholar 

14. Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C. (eds.): Selected Papers on Automath. North-Holland, Amsterdam (1994)

    MATH  Google Scholar 

15. Paulson, L.C.: Isabelle: A Generic Theorem Prover (with a contribution by T. Nipkow). Lecture Notes in Computer Science, vol.  828. Springer, Berlin (1994)

    Google Scholar 

16. Paulson, L.C.: A generic tableau prover and its integration with Isabelle. J. Univers. Comput. Sci. 5(3), 73–87 (1999)

    MATH  MathSciNet  Google Scholar 

17. Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, Amsterdam (2001)

    Google Scholar 

18. Skolem, Th.: Logisch-Kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit Mathematischen Sätze nebst einem Theoreme über Dichte Mengen, Skrifter I, 4, 1–36, Det Norske Videnskaps-Akademi, 1920. In: Fenstad, J.E. (ed.) Selected Works in Logic, pp. 103–136. Universitetsforlaget, Oslo (1970)

19. Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177–203 (1998)

    Article  MATH  MathSciNet  Google Scholar 

20. Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35–48 (2006)

    MATH  MathSciNet  Google Scholar 

21. The Coq development team. The Coq Proof Assistant Reference Manual, version 8.1, 2006. http://coq.inria.fr/.

Download references