Cyrus F Nourani

MIM and Morph Gentzen Logik

Standard-Icon

Standard-Icon

PrintPrint
Englische Version

netzspannung.org

Dateien

Kurzbeschreibung

The Morph Gentzen Computing Techniques

The Morphe Gentzen computing technques for multimedia are new projects with important computing applications since [Nourani 1998a,b]. The basic principles are a mathematical logic where a Gentzen [Getnzen 1943] or natural deduction systems are defined by taking arbitrary structures and multimedia objects coded by diagram functions. Multimedia objects are viewed as syntactic objects defined by functions, to which the deductive system is applied. Thus we define a syntactic morphing to be a technique by which multimedia objects and hybrid pictures are homomorphically mapped via their defining functions to a new hybrid picture. Functorial topological structures can be defined without difficulty. The deduction rules are a Gentzen system augmented by Morphing, and Trans-morphing. The logical language has function names for hybrid pictures.

The Morph Rule - An object defined by the functional n-tuple <f1,...,fn> can be Morphed to an object defined by the functional n-tuple <h(f1),...,h(fn)>, provided h is a homomrphism of abstract signature structures.

The TransMorph Rules- A set of rules whereby combining hybrid pictures p1,...,pn defines an Event {p1,p2,...,pn} with a consequent hybrid picture p. Thus the combination is an impetus event. By trans-morphing hybrid picture's corresponding functions a new hybrid picture is deduced. The techniques can be applied to arbitrary topological structures. The languages and MIM rules are applied to algebraic structures. The deductive theory is a Gentzen system in which hybrid pictures are named by parameterized functions; augmented by the morph and trans-morph rules. The Model theory is defined from Intelligent syntax languages[96a]. A computational logic for intelligent languages is presented in brief with a soundness and completeness theorem in [Nourani 1998a]. The idea is to do it at abstract models syntax trees without specifics for the shapes and topologies applied. With well-behaved infinitary languages the enclosed basis is attained.

Theorem [Nourani 1997] Morph Gentzen Logic is sound and complete.
References
Nourani,C.F.,1998a "MIM Logik," Summer Logic Colloquium, August 1998, Prague.
Gentzen, G, Beweisbarkeit und Unbewiesbarket von Anfangsfallen der trasnfininten Induktion in der reinen Zahlentheorie, Math Ann 119, 140-161,1943.
Nourani,C.F.1998b," Intelligent Multimedia," 1996, Intelligence and Multimedia Applications - 1998. February 1998, Monash University, Victoria - 3842, Australia. Poster Announcement.
Nouran,C.F.1999 "Intelligent Multimdia- New Computing Techniques and Its Applications, " CSIT, January 1999, Moscow.
Nourani,C.F. 1998c, Creating Digital Art and Motion Pictures with Intelligent Multimedia,
A chapter in Intelligent Multimedia, Treeless Press, February 2000. www.treelesspress.com



KünstlerInnen / AutorInnen

Entstehung

Vereinigte Staaten, 1997-2002

Partner / Sponsoren

Kommentar

Morphed Gentzen Virtual Computing
Cyrus F.Nourani
November 18, 1998

1. Morph Gentzen
MIM- The IM Morphed Computing Logic Logics for computing for multimedia are new projects with important computing applications since [Nourani 97]. The basic principles are a mathematical logic where a Gentzen or natural deduction systems is defined by taking arbitrary structures coded by diagram functions. The techniques can be applied to arbitrary topological structures. Thus we define a syntactic morphing to be a technique by which infinitary definable structures are homomorphically mapped via their defining functions to new structures. The deduction rules are a Gentzen system augmented by two rules Morphing, and Trans-morphing. The Morph Rule - A structure defined by the functional n-tuple <f1,...,fn> can be Morphed to a structures definable by the functional n-tuple <h(f1),...,h(fn)>, provided h is a homomrphism of abstract signature structures[Nourani 96]. The TransMorph Rules- A set of rules whereby combining structures A1,...,An defines an Event {A1,A2,...,An} with a consequent structure B. Thus the combination is an impetus event. The deductive theory is a Gentzen system in which structures named by parameterized functions; augmented by the morph and trans-morph rules. The structures we apply the Morph logic to are definable by positive diagrams. The idea is to do it at abstract models syntax trees without specifics for the shapes and topologies applied. We start with Lw1w, and further on might apply well-behaved infinitary languages.

Theorem 1- Soundness and Completeness- Morphed Gentzen Logic is sound and complete.

2. Plan Algebras and G-Diagrams
A plan is a sequence of operations in the universe that could result in terms that instantiate the truth of the goal formulas in the universe. That's what goes on as far as the algebra of the model is concerned. Generic diagrams, G-diagrams, e.g Nourani 95, are used to build models with a minimal family of generalized Skolem functions. The minimal set of function symbols are those with which a model can be built inductively. It is a new view of planning prompted by our method of planning with G-diagrams and virtual Skolemized trees. It is a model-theoretic view. Proof-theoretically a plan is the sequence of proof steps(Fiks-Nils 1971) that yields the proof for the goal formula. In planning with G-diagrams that part of the plan that involves virtual Skolemnized trees is carried along with the proof tree for a plan goal. By allowing proof-tree leaves get instantiated with non-atomic formulas, we get a more general notions of a proof. In our 1994 on paper we also instantiate proof tree leaves with virtual Skolemized trees. Thus virtual trees are substituted for the leaves. By a virtual tree we intend a term made of constant symbols and Skolem functions terms. Existentially quantified diagrams carry a main deficit- the Skolemized formulas are not characterized. Hilbert's epsilon symbol may be applied to solve this problem. We then define Hilbert models to handle the proof-model problems further on. The idea is that if the virtual proof tree is constructed then the plan has a model in which the goals are satisfied. The model is the initial model of the AI world for which the virtual Skolemized trees were constructed. Thus we the following Virtual Proof Tree Sound Computing Theorem.
Theorem 2 For the virtual proof trees defined for a goal formula from the G-diagram there is an initial model satisfying the goal formulas. It is the initial model definable by the G-diagram.
The presents techniques establish a correspondence from virtual proof trees to Hilbert models.
Theorem 3 The Hilbert's epsilon technique implies there is a model M for
the set of formulas such that we can take an existentially quantified
formula w[X] and have it instantiated by a Skolem function which can
answer the satisfiability question for the model.

Alternate Project_METAAI@CompuServe.com
Copyright © Photo reproduction for noncommercial use and conference publications is permitted without payment of royalty provided that the Journal reference and copyright notice are included on the first page.
USA Academic Address UCSB when at Univeristy
References
Gentzen, G, Beweisbarkeit und Unbewiesbarket von Anfangsfallen der trasnfininten Induktion in der reinen
Zahlentheorie, Math Ann 119, 140-161,1943.
Nourani,C.F., MIM Logik, 1997, ASL, Prague, August 1998.
Fiks-Nils 1971, Fikes, R.E. and N.J. Nilsson, "Strips: A New Approach to the Application of Theorem Proving to Problem Solving," AI 2,, 1971, pp. 189-208.
ADJ 1973, Goguen, J.A., J.W. Thatcher, E.G. Wagner, and J.B. Wright, A Junction Between Computer Science and Category Theory, IBM Research Report RC 4526, 1973.
Nourani,C.F. 1994, GF-Diagrams For Models and Free Proof Trees, March 26, 1994, Abstract Presented at the Berlin Logic Colloquium, May 1994.
Nourani,C.F.1995, Free Proof Trees And Model-Theoretic Planning,AISB, Sheffield, England, April 1995.
Nourani, C.F. 1996, Slalom Tree Computing, AI Comm., The European Journal on AI, vol. 9., no. 4, December 1996.






Eingabe des Beitrags

Cyrus F 'Kris' Nourani, 04.05.2002

Kategorie

Schlagworte

Ergänzungen zur Schlagwortliste