## Literature concerning AEtnaNova/Referee and its underlying logic

- ### Published:

  - E.G.Omodeo, D.Cantone, A.Policriti, and J.T.Schwartz. A computerized Referee. In: O. Stock and M. Schaerf (eds.), "Reasoning, Action and Interaction in AI Theories and Systems", Essays dedicated to Luigia Carlucci Aiello, Springer-Verlag, Berlin. Lecture Notes in Artificial Intelligence, vol.4155, pp.114-136, 2006.
  - D.Cantone, E.G.Omodeo, J.T.Schwartz, and P.Ursino. Notes from the logbook of a proof-checker's project. In N. Dershowitz ed., International symposium on verification (Theory and Practice) celebrating Zohar Manna's 10000002-th birthday. Springer-Verlag, LNCS, vol.2772, pp.214-230, 2003.
  - E.G.Omodeo, J.T.Schwartz. A 'Theory' mechanism for a proof-verifier based on first-order set theory. In: A. Kakas and F. Sadri (eds.), "Computational Logic: Logic Programming and beyond", Essays in honour of Robert Kowalski, part II, Springer-Verlag, Berlin. Lecture Notes in Artificial Intelligence, vol.2408, pp.214-230, 2002.

- ### Conference presentations:

  - D.Cantone, A.Formisano, E.G.Omodeo, and J.T.Schwartz. Various commonly occurring decidable extensions of multi-level syllogistic. In S.Ranise and C.Tinelli, eds., Proceedings of the workshop on Pragmatics of Decision Procedures in Automated Reasoning 2003 PDPAR'03 (CADE 19). July 29, 2003 Miami, USA.

- ### In progress:

  - J.T. Schwartz, D. Cantone, and E.G. Omodeo. Computational logic and set theory. Book to be published with Springer-Verlag.
  - E. G. Omodeo, Alexandru Ian Tomescu. Modeling CNF-formulae and formally proving the correctness of DPLL by means of Referee. Submitted, 2007.
  - D. Cantone, C. Chiaruttini, Marianna Nicolosi Asmundo, E.G. Omodeo. Cumulative hierarchies and computability over universes of sets. Submitted, 2007.
  - D. Cantone, C. Chiaruttini, Marianna Nicolosi Asmundo, E.G. Omodeo. Gerarchie cumulative e computabilità sopra universi di insiemi. Technical report of "Dipartimento di Matematica e Informatica", University of Trieste (Italy), 2007.

- ### Historical:

  - D. Cantone, E.G. Omodeo, and A.Policriti. Set Theory for Computing - From decision procedures to declarative programming with sets. Springer-Verlag, Texts and Monographs in Computer Science, 2001.
  - D. Cantone, A. Ferro, and E.G. Omodeo. "Computable Set Theory," Vol.1., Oxford University Press, International Series of Monographs on Computer Science, 347 pp., 1989.
  - M. Breban, A. Ferro, E.G. Omodeo, and J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Communications on Pure and Applied Mathematics, 34, pp.177--195, 1981.
  - A. Ferro, E.G. Omodeo, and J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions. Communications on Pure and Applied Mathematics, John Wiley & Sons, New York, 33, pp.599--608, 1980.
  - A. Ferro, E.G. Omodeo, and J.T. Schwartz. Decision procedures for some fragments of set theory. Proceedings of the 5th conference on Automated Deduction, pp.88--96. Lecture Notes in Computer Science, 87, Springer--Verlag, Berlin--Heidelberg--New York, 1980.
  - M. Davis, J. T. Schwartz. TO BE COMPLETED
  - J. T. Schwartz. TO BE COMPLETED
  - Martin Davis, Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960.
  - M. Davis, G. Logemann, D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962.

- ### Relevant, though not directly related to the system:

  - Nelson Dunford, Jacob T. Schwartz. Linear operators. Part I: General theory, with the assistance of William G. Bade and Robert G. Bartle. New York, Interscience Publishers, 1958. 14+858 pp.
  - Edmund Yehezkel Landau. Foundations of Analysis: The Arithmetic of Whole, Rational, Irrational and Complex Numbers (trans. F. Steinhardt). Chelsea Publishing Company, New York, 1951.