Comparing CycL and IFF

 

Cyc

Cyc is the name of a very large, multi-contextual knowledge base and inference engine, the development of which started at the Microelectronics and Computer Technology Corporation (MCC) in Austin, Texas during the early 1980s. According to Cycorp, the company based in Austin, Texas, that is developing the Cyc project, Cyc began as a dream to create a computerized encyclopedia. Cyc is an attempt to do symbolic artificial intelligence on a massive scale. Its avowed purpose is to break the software brittleness bottleneck once and for all by constructing a foundation of basic "common sense" knowledge. All of the knowledge in Cyc is represented declaratively in the form of logical assertions. Cyc assertions include

1.      simple statements of fact,

2.      rules about what conclusions to draw if certain statements of fact are satisfied (true), and

3.      rules about how to reason with certain types of facts and rules.

The Cyc inference engine using deductive reasoning derives new conclusions.

 

CycL

Cycorp represents its knowledge in a form of predicate logic known as CycL, which is a superset of KIF. CycL is the representation language of Cyc. CycL, the Cyc representation language, is a form of first order predicate logic, with equality, augmentations for default reasoning, skolemization, and some second-order features (e.g., quantification over predicates is allowed in some circumstances). It uses a form of circumscription, includes the unique names assumption, and can make use of the closed world assumption where appropriate. The document: http://www.cyc.com/cycl.html gives an overview of the language.

A set of CycL sentences forms a knowledge base Cyc KB. There is a kernel knowledge base CycL Kernel KB that is in common among all Cyc knowledge bases. The kernel knowledge base is important because it includes some axioms as well as the hierarchy of collections and individuals. A Cyc knowledge base is thought of as a large collection of Cyc assertions. Cyc assertions correspond to IFF expressions. Inference in Cyc is a general logical deduction. Outside the assertion collection are all the Cyc constants. Cyc constants correspond to IFF types and instances. A Cyc constant is linked to all the assertions in the knowledge base that reference that constant. Each assertion in the knowledge base can itself be treated as a constant, having its own links to other assertions that reference it. In much the same way each IFF expression is regarded to be an IFF relation type. The following hierarchy is a rough breakdown of the constant terms in the Cyc knowledge base.

·         Categories

○        Categories of categories

○        Categories of individuals

○        Categories of actions (script types)

·         Predicates and Functions

·         Attributes

online casino

·         Lexical objects

·         Proper nouns

·         Microtheories (contexts)

The following diagram gives a rough idea of the relationships between the top-level types in Cyc.

 

The following table gives correspondences between basic notions of CycL and IFF.

Basic Notions

CycL

Onto Logic

constant     #$Collection

type     ent(A)+indiv(A)+rel(A)

 

entity type     α Î ent(A)

individual     #$Individual

individual     a Î indiv(A)

predicate     #$Predicate

relation type     ρ Î rel(A)

predicate arity

relation arity     arity(ρ)

predicate argument types

relation signature     A(ρ)

variable

variable     x Î var

formula     #$CycFormula

expression     φ Î expr(typ(A))

ground atomic formula

relation classification (relationship)    ⊨A ρ

microtheory or context

ontology (ontological theory)     O

CycL knowledge base (KB)

ontological model     A

The following table gives correspondences between relations of CycL and IFF.

Structural relation types

CycL

Onto Logic

#$isa(#$ReifiableTerm, #$Collection)

classification relation ⊨A of some model A

#$genls(#$Collection, #$Collection)

entails (subtype) ⊢

#$arity(#$Relationship, #$Integer)

valence

#$argnIsa(#$Relationship, #$Collection)

A(φ)n, the signature function

#$ist(#$Microtheory, #$CycFormula)

satisfies, consequence ⊢

O ⊢ φ when clo(O) ' φ

#$genlMt(#$Microtheory, #$Microtheory)

ontology (truth lattice) order:

O1 £ O2 when clo(O1) Ê clo(O2)

O1 £ O2 and O2 ⊢ φ implies O1 ⊢ φ

#$genlPreds(#$Predicate, #$Predicate)

expression order:

φ1 £ φ2 when clo(φ1) ' φ2

 

 

é

Please send questions, comments and suggestions about this page to: Robert E. Kent rekent@ontologos.org

Copyright © 2000 TOC (The Ontology Consortium). All rights reserved. Revised: July 2000