Geri Dön

HOL90 sistemi x windows kullanıcı arayüzü

Başlık çevirisi mevcut değil.

  1. Tez No: 66430
  2. Yazar: TAMER SEZGİN
  3. Danışmanlar: PROF. DR. EMRE HARMANCI
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 1997
  8. Dil: Türkçe
  9. Üniversite: İstanbul Teknik Üniversitesi
  10. Enstitü: Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Kontrol ve Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Kontrol ve Bilgisayar Mühendisliği Bilim Dalı
  13. Sayfa Sayısı: 98

Özet

ÖZET Bu projenin amacı, akademik ortamlarda, özellikle Edinburgh Üniversitesi ve Cambridge Üniversitesinde yürütülen bilgisayar destekli yüksek dereceli mantık (Higher Order Logic) çalışmalarının bir sonucu olan ve halen geliştirilmesi devam eden HOL sistemine bir kullanıcı arayüzü yazılmasıdır. HOL sisteminin amacı, mantıksal tanıtlamaların yapılabileceği, daha önce tanıtlanmış teoremlerin tekrar kullanılabilecek bir yapıda tutulabileceği, ve yeni teoremlerin daha sonra tekrar kullanılabilecek şekilde saklanabileceği bir ortam oluşturmaktır. HOL programı, ilk olarak LISP üzerinde yazılmış, daha sonra, gene Edinburgh Üniversitesinde geliştirilen ML (Meta Language) üzerine taşınmış, son olarak ta, ML'nin New Jersey Üniversitesi tarafından geliştirilen yeni bir sürümü olan SML/NJ üzerine taşınmıştır. ML üzerinde çalışan sürümü HOL88, SML/NJ üzerinde çalışan son sürümü ise HOL90 olarak bilinir. HOL'ün üzerinde çalıştığı sistemler (LISP, ML, SML) genellikle kullanıcının etkileşimli olarak çalıştığı ortamlardır. Başka bir ifadeyle, bir komut yazılır ve bilgisayarın ürettiği yanıt hemen alınır. Yalnız, programın birçok ortamda çalışabilmesi için kullanıcıya kolaylık sağlayacak iyi bir grafik kullanıcı arayüzü bulunmamaktadır. Ayrıca sistemi kullanabilmek için, tüm HOL komutlarının isimlerini, parametrelerini ve bu parametrelerin tiplerini bilmek gerekir. Bütün bunları ezberlemek ise sürekli genişleyen bir sistem için mantıklı değildir. Bu sorunlara cevap vermek üzere yazılmış olan birkaç program vardır fakat, gene yüksek düzeyli makro diller kullanıldığından zaten çok kaynak isteyen HOL'ü çalıştırabilmek için gerekli olan kaynak miktarı iyice artmakta, ve bu günkü masa üstü bilgisayarlar için bu sistemler oldukça hantal kalmaktadır. Bu nedenle yazılması kararlaştırılan program, bir UNLX türevi olan Linux işletim sistemi üzerinde X Window System ortamında çalışan ve yukarıda anlatılan sorunlara çözüm getirmeye çalışan bir programdır. Program C++ dilinde, Qt sınıf kütüphanesi kullanılarak geliştirilmiştir. VI

Özet (Çeviri)

SUMMARY The purpose of this project is to develop a graphical user interface program for HOL (Higher Order Logic) system which was developed in Edinburgh University and Cambridge University as a result of computer aided higher order logic studies. The purpose of the HOL system is to bring an environment in which teorem proving problems can be solved, the resulting theorems of previous studies can be reused and the new theories can be developed in such a way that thay can be used later. HOL system was originally developed in LISP language. Later with the development of ML (Meta Language) in Edinburgh University, this system was ported to ML and called HOL88, and finally when a new version of ML, called SML/NJ, developed in New Jersey University, last version of HOL was released with the name“HOL90”. The subsystems that HOL operates on (LISP, ML, SML), are genreally interactive environments, that is, a command is entered and response is produced by the computer before it prompts for the next command. In such an environment it is very tedious to produce and maintain large programs. Although thare are facilities to save these programs in disk files and later restore them to the environment. For interactively proving theorems, there is no practical and user friedly way of usig HOL. Also, you always have to work with manuals of HOL for typing function names, parameter order and parameter types correctly, or you have to memorize most of them. Although, it is possible to memorize the HOL command set and parameters, for such a continually developing and changing program it is not very logical. After all, when next version is released, all the synthatic rules may be changed. To address, these problems, some work has been done. But since macro languages are used, the resulting code is huge: And this increases the requirements of the HOL system even more. These requirements are relatively very high for a standard desktop personal computer. The aim of the program written during the project is ease the above problems. For development environment, Linux operating system and X Window System were used. The program was developed in C++ language. Since X system does not directly provide a user interface object set, and does not have C++ support very well, Qt class library for C++ was used. vu

Benzer Tezler

  1. Tez No

    789940

    An experimental evaluation of relative reconstruction algorithms

    Göreli rekonstrüksiyon algoritmalarının deneysel değerlendirmesi

    YAKUP GENÇ

    Yüksek Lisans

    İngilizce

    İngilizce

    1995

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolUniversity of Illinois at Urbana-Champaign

    Bilgisayar Bilimleri Ana Bilim Dalı

    PROF. DR. JEAN PONCE

Geri Dön