More on the Structure of the Verifier System

  • Jacob T. Schwartz
  • Domenico Cantone
  • Eugenio G. Omodeo


This chapter describes in detail the set-based proof-verification system Ref, developed by the authors, and its underlying design. The chapter falls into two parts: (i) An account of the general syntax and overall structure of proofs acceptable to the verifier. (ii) A listing of the mechanisms actually chosen from the list of candidate inference mechanisms surveyed earlier in the book, for inclusion in the verifier’s initial endowment. The syntax used to invoke each of the verifier’s built-in inference mechanisms is explained.

The most central among the chosen inference primitives is named ELEM. Its use is, often, tacitly combined with other forms of inference. ELEM implements multi-level syllogistic, a decision algorithm which determines whether a given unquantified set-theoretic formula involving individual variables (which designate sets) and a restricted collection of set operators is satisfiable.


Function Symbol Monotonicity Property Inference Mechanism Syntax Tree Proof Step 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [FO10]
    Formisano, A., Omodeo, E.: Theory-specific automated reasoning. In: Dovier, A., Pontelli, E. (eds.) A 25-Year Perspective on Logic Programming—Achievements of the Italian Association for Logic Programming, GULP. LNCS, vol. 6125, pp. 37–63. Springer, Berlin (2010). Chap. 3 CrossRefGoogle Scholar
  2. [OS02]
    Omodeo, E.G., Schwartz, J.T.: A ‘Theory’ mechanism for a proof-verifier based on first-order set theory. In: Kakas, A., Sadri, F. (eds.) Computational Logic: Logic Programming and beyond—Essays in honour of Bob Kowalski, Part II, vol. 2408, pp. 214–230. Springer, Berlin (2002) CrossRefGoogle Scholar
  3. [Wol03]
    Wolfram, S.: The Mathematica Book, 5th edn., p. 1464. Wolfram Media, Champaign (2003) Google Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.New York UniversityNew YorkUSA
  2. 2.Dept. of Mathematics & Computer ScienceUniversity of CataniaCataniaItaly
  3. 3.Dept. of Mathematics & Computer ScienceUniversity of TriesteTriesteItaly

Personalised recommendations