ANSI INCITS ISO IEC 24707-2007 Information technology Common Logic (CL) a framework for a family of logic-based languages.pdf

1、INCITS/ISO/IEC 24707:20072008 (ISO/IEC 24707:2007, IDT) Information technology Common Logic (CL): a frameworkfor a family of logic-based languagesINCITS/ISO/IEC 24707:20072008(ISO/IEC 24707:2007, IDT)INCITS/ISO/IEC 24707:20072008 ii ITIC 2008 All rights reserved PDF disclaimer This PDF file may cont

2、ain embedded typefaces. In accordance with Adobes licensing policy, this file may be printed or viewed but shall not be edited unless the typefaces which are embedded are licensed to and installed on the computer performing the editing. In downloading this file, parties accept therein the responsibi

3、lity of not infringing Adobes licensing policy. The ISO Central Secretariat accepts no liability in this area. Adobe is a trademark of Adobe Systems Incorporated. Details of the software products used to create this PDF file can be found in the General Info relative to the file; the PDF-creation par

4、ameters were optimized for printing. Every care has been taken to ensure that the file is suitable for use by ISO member bodies. In the unlikely event that a problem relating to it is found, please inform the Central Secretariat at the address given below. Adopted by INCITS (InterNational Committee

5、for Information Technology Standards) as an American National Standard. Date of ANSI Approval: 7/1/2008 Published by American National Standards Institute, 25 West 43rd Street, New York, New York 10036 Copyright 2008 by Information Technology Industry Council (ITI). All rights reserved. These materi

6、als are subject to copyright claims of International Standardization Organization (ISO), International Electrotechnical Commission (IEC), American National Standards Institute (ANSI), and Information Technology Industry Council (ITI). Not for resale. No part of this publication may be reproduced in

7、any form, including an electronic retrieval system, without the prior written permission of ITI. All requests pertaining to this standard should be submitted to ITI, 1250 Eye Street NW, Washington, DC 20005. Printed in the United States of America INCITS/ISO/IEC 24707:20072008 ITIC 2008 All rights r

8、eserved iii Contents Page Foreword vi Introduction . vii 1 Scope 1 2 Normative references .2 3 Terms and definitions 2 4 Symbols and abbreviations .5 4.1 Symbols 5 4.2 Abbreviations .6 5 Requirements and design overview 6 5.1 Requirements .6 5.2 A family of notations 8 6 Common Logic abstract syntax

9、 and semantics 8 6.1 Common Logic abstract syntax. 8 6.2 Common Logic semantics . 13 6.3 Importing and identification on a network 16 6.4 Satisfaction, validity and entailment. 18 6.5 Sequence markers, recursion and argument lists: discussion 18 6.6 Special cases and translations between dialects .

10、19 7 Conformance 20 7.1 Dialect conformance 20 7.2 Application conformance . 22 7.3 Network conformance 22 Annex A (normative) Common Logic Interchange Format (CLIF) 23 A.1 Introduction 23 A.2 CLIF Syntax 24 A.3 CLIF semantics . 29 A.4 CLIF conformance 32 Annex B (normative) Conceptual Graph Interch

11、ange Format (CGIF) . 33 B.1 Introduction 33 B.2 CG Core Syntax and Semantics. 39 B.3 Extended CGIF Syntax . 45 B.4 CGIF conformance . 51 Annex C (normative) eXtended Common Logic Markup Language (XCL) 54 C.1 Introduction 54 C.2 XCL Syntax . 54 C.3 XCL Semantics . 72 C.4 XCL Conformance 72 Bibliograp

12、hy 73 Figures Page Figure 1 Structure of a text and the taxonomy of the phrase category text 10 INCITS/ISO/IEC 24707:20072008 iv ITIC 2008 All rights reserved Figure 2 Abstract syntax of sentence and its sub-categories . 10 Figure 3 Abstract syntax of a module 10 Figure 4 Abstract syntax of a quanti

13、fied sentence . 11 Figure 5 Abstract syntax of a boolean sentence 11 Figure 6 Abstract syntax of an atom . 12 Figure 7 Abstract syntax of a term and term sequence 12 Tables Page Table 1 Interpretations of Common Logic Expressions 15 Table A.1 CLIF Semantics 30 Table A.2 Mapping from additional CLIF

14、forms to core CLIF forms 31 Table B.1 Mapping from CL abstract syntax to extended CGIF syntax 52 INCITS/ISO/IEC 24707:20072008 ITIC 2008 All rights reserved v Foreword ISO (the International Organization for Standardization) and IEC (the International Electrotechnical Commission) form the specialize

15、d system for worldwide standardization. National bodies that are members of ISO or IEC participate in the development of International Standards through technical committees established by the respective organization to deal with particular fields of technical activity. ISO and IEC technical committ

16、ees collaborate in fields of mutual interest. Other international organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work. In the field of information technology, ISO and IEC have established a joint technical committee, ISO/IEC JTC 1. International

17、Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 2. The main task of the joint technical committee is to prepare International Standards. Draft International Standards adopted by the joint technical committee are circulated to national bodies for voting. Publi

18、cation as an International Standard requires approval by at least 75 % of the national bodies casting a vote. Attention is drawn to the possibility that some of the elements of this document may be the subject of patent rights. ISO and IEC shall not be held responsible for identifying any or all suc

19、h patent rights. ISO/IEC 24707 was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology, Subcommittee SC 32, Data management and interchange. INCITS/ISO/IEC 24707:20072008 vi ITIC 2008 All rights reserved Introduction Common Logic is a logic framework intended for information

20、exchange and transmission. The framework allows for a variety of different syntactic forms, called dialects, all expressible within a common XML-based syntax and all sharing a single semantics. Common Logic has some novel features, chief among them being a syntax which is signature-free and permits

21、higher-order constructions such as quantification over classes or relations while preserving a first-order model theory, and a semantics which allows theories to describe intensional entities such as classes or properties. It also fixes the meanings of a few conventions in widespread use, such as nu

22、merals to denote integers and quotation marks to denote character strings, and has provision for the use of datatypes and for naming, importing and transmitting content on the World Wide Web using XML. AMERICAN NATIONAL STANDARD INCITS/ISO/IEC 24707:20072008 ITIC 2008 All rights reserved 1 Informati

23、on technology Common Logic (CL): a framework for a family of logic-based languages 1 Scope This International Standard specifies a family of logic languages designed for use in the representation and interchange of information and data among disparate computer systems. The following features are ess

24、ential to the design of this International Standard: Languages in the family have declarative semantics. It is possible to understand the meaning of expressions in these languages without appeal to an interpreter for manipulating those expressions. Languages in the family are logically comprehensive

25、 at its most general, they provide for the expression of arbitrary first-order logical sentences. Interchange of information among heterogeneous computer systems. The following are within the scope of this International Standard: representation of information in ontologies and knowledge bases; speci

26、fication of expressions that are the input or output of inference engines; formal interpretations of the symbols in the language. The following are outside the scope of this International Standard: the specification of proof theory or inference rules; specification of translators between the notatio

27、ns of heterogeneous computer systems; computer-based operational methods of providing relationships between symbols in the logical universe of discourse and individuals in the real world. This International Standard describes Common Logics syntax and semantics. It defines an abstract syntax and an a

28、ssociated model-theoretic semantics for a specific extension of first-order logic. The intent is that the content of any system using first-order logic can be represented in this International Standard. The purpose is to facilitate interchange of first-order logic-based information between systems.

29、Issues relating to computability using this International Standard (efficiency, optimization, etc.) are not addressed. INCITS/ISO/IEC 24707:20072008 2 ITIC 2008 All rights reserved 2 Normative references The following referenced documents are indispensable for the application of this document. For d

30、ated references, only the edition cited applies. For undated references, the latest edition of the referenced document (including any amendments) applies. ISO/IEC 2382-15:1999, Information technology Vocabulary Part 15: Programming languages ISO/IEC 10646:2003, Information technology Universal Multi

31、ple-Octet Coded Character Set (UCS) ISO/IEC 14977:1996, Information technology Syntactic metalanguage Extended BNF 3 Terms and definitions For the purposes of this document, the following terms and definitions apply. 3.1 atom sentence form which has no subsentences as syntactic components NOTE Can b

32、e either an equation, or an atomic sentence consisting of a predicate applied to an argument sequence. 3.2 axiom any sentence which is assumed to be true, from which others are derived, or by which they are entailed NOTE In a computational setting, an axiom is a sentence which is never posed as a go

33、al to be proved, but only used to prove other sentences. 3.3 Common Logic Interchange Format CLIF KIF-based syntax that is used for illustration purposes in this International Standard NOTE It is one of the concrete syntaxes as described in Annex A. The name KIF is not used for this syntax in order

34、to distinguish it from the commonly used KIF dialects. No assumptions are made in this International Standard with respect to KIF semantics; in particular, no equivalence between CLIF and KIF is intended. 3.4 conceptual graph CG graphical or textual display of symbols arranged according to the style

35、 of conceptual graph theory 3.5 Conceptual Graph Interchange Format CGIF text version of conceptual graphs whose rules of formation conform to Annex B of this International Standard NOTE Sometimes may refer to an example of a character string that conforms to Annex B. Intended to convey exactly the

36、same structure and semantics as an equivalent conceptual graph. 3.6 conceptual graph theory form of first-order logic which represents existential quantification and conjunction via the assertion of logical constructs called concepts and relations, which are arranged in an abstract or visually displ

37、ayed graph NOTE Conceptual graph theory was introduced by John Sowa 1. INCITS/ISO/IEC 24707:20072008 ITIC 2008 All rights reserved 3 3.7 denotation relationship holding between a name or expression and the thing to which it refers NOTE Also used, with of, to mean the entity being named, i.e. the ref

38、erent of a name or expression. 3.8 dialect concrete instance of Common Logic syntax that shares (at least some of) the uniform semantics of Common Logic NOTE A dialect may be textual or graphical or possibly some other form. A dialect by definition is also a conforming language (see 7.1 for further

39、details). 3.9 discourse name name whose interpretation is in the universe of discourse NOTE There is no assumption that different names are interpreted as different individuals. A single individual in the universe of discourse may be denoted by two or more distinct names. 3.10 domain of discourse Se

40、e universe of discourse. 3.11 eXtensible Common Logic Markup Language XCL XML-based syntax for Common Logic 3.12 individual one element of the universe of discourse NOTE The universe of discourse is the set of all individuals. 3.13 Internationalized Resource Identifier IRI string of Unicode characte

41、rs conforming to the syntax described in 2 and intended for use as an Internet network identifier syntax which can accommodate a wide variety of international character forms NOTE Intended to replace Uniform Resource Identifier as an Internet standard for network identifiers. 3.14 interpretation for

42、mal specification of the meanings of the names in a vocabulary of a Common Logic dialect in terms of a universe of reference. NOTE 1 An interpretation in turn determines the semantic values of all complex expressions of the dialect, in particular the truth values of its sentences. NOTE 2 See 6.2 for

43、 a more precise description of how an interpretation is defined. 3.15 Knowledge Interchange Format KIF text-based first order formalism, using a LISP-like list notation NOTE 1 KIF, introduced by Mike Genesereth 3, originated with the Knowledge Sharing Effort sponsored by the US DARPA. NOTE 2 KIF for

44、ms the basis for one of the three Common Logic dialects included in this International Standard. INCITS/ISO/IEC 24707:20072008 4 ITIC 2008 All rights reserved 3.16 operator distinguished syntactic role played by a specified component within a functional term NOTE The denotation of a functional term

45、in an interpretation is determined by the functional extension of the denotation of the operator together with the denotations of the remaining components. 3.17 predicate Common Logic distinguished syntactic role played by exactly one component within an atomic sentence NOTE The truth value of an at

46、omic sentence in an interpretation is determined by the relational extension of the denotation of the predicate together with the denotations of the remaining components. 3.18 segregated dialect dialect in which some names are non-discourse names NOTE In an interpretation of a segregated dialect, th

47、e denotations of the non-discourse names are in the universe of reference, but not in the universe of discourse. 3.19 sentence Common Logic unit of logical text which is true or false, i.e. which is assigned a truth-value in an interpretation 3.20 sort any subset of the universe of discourse over wh

48、ich some quantifier is allowed to range NOTE Related to the definition of type (see 3.24). Generally used to mean a proper subset of the individuals in the universe of discourse. 3.21 sorted logic logic system (whether first-order or not) which requires that all nonlogical symbols be assigned to a s

49、ort 3.22 term Common Logic expression which denotes an individual, consisting of either a name or, recursively, a function term applied to a sequence of arguments, which are themselves terms 3.23 traditional first-order logic TFOL traditional mathematical formulations of logic as introduced chiefly by Russell, Whitehead, Peano, Frege, Peirce and Tarski dealing with n-ary predication, the Boolean operators (including negation) and quantification, and