Proof-Checking Process-Based Reasoning about Physical Systems

E. Uçar, V. Akman, Bilkent Üniversitesi, Türkiye.

Abstract

Having the most sophisticated set of modeling features and the most complete ontology, Forbus Qualitative Process Theory allows better explanations of device behaviour than other systems because, for example, processes can explicitly be discussed. It can reason about state changes such as turning water to stearn which can be at best implicitly represented in other systems. Forbus displays logical translations of selected process and individual view descriptions but does not attempt to axiomatize the whole theory. We believe that it is necessary to provide such a formalization. The Boyer-Moore Theorem Prover is one of the best media to do so.

Özet

En karmaşık modelleme özelliklerine ve en eksiksiz ontolojiye sahip olan Forbus Niteliksel İşlem Teorisi, cihaz davranışının diğer sistemlerden daha iyi şekilde açıklanmasına izin verir, çünkü örneğin süreçler açıkça tartışılabilir. Diğer sistemlerde en iyi örtük şekilde temsil edilebilecek olan suyun buhara dönüşmesi gibi durum değişikliklerine neden olabilir. Forbus, seçilen sürecin ve bireysel görünüm tanımlarının mantıksal tercümelerini gösterir, ancak tüm teoriyi aksiyomize etmeye çalışmaz. Böyle bir formalizasyon sağlamanın gerekli olduğuna inanıyoruz. Boyer-Moore Teoremi Prover, bunu yapacak en iyi medyalardan biri.

Tam Metin

Bildirinin tamamını görüntülemek için aşağıdaki dosyayı indiriniz.

12MB

25-32-Proof-Checking Process-Based Reasoning about Physical Systems.pdf

PDF

Open