More on the Structure of the Verifier System
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.
KeywordsFunction Symbol Monotonicity Property Inference Mechanism Syntax Tree Proof Step
- [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
- [Wol03]Wolfram, S.: The Mathematica Book, 5th edn., p. 1464. Wolfram Media, Champaign (2003) Google Scholar