An ATP of a Relational Proof System for Order of Magnitude Reasoning with Negligibility, Non-closeness and Distance

In Tu-Bao Ho & Zhi-Hua Zhou (eds.), PRICAI 2008: Trends in Artificial Intelligence. Springer. pp. 128--139 (2008)
  Copy   BIBTEX


We introduce an Automatic Theorem Prover (ATP) of a dual tableau system for a relational logic for order of magnitude qualitative reasoning, which allows us to deal with relations such as negligibility, non-closeness and distance. Dual tableau systems are validity checkers that can serve as a tool for verification of a variety of tasks in order of magnitude reasoning, such as the use of qualitative sum of some classes of numbers. In the design of our ATP, we have introduced some heuristics, such as the so called phantom variables, which improve the efficiency of the selection of variables used un the proof.



    Upload a copy of this work     Papers currently archived: 93,296

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Reasoning with Qualitative Velocity: Towards a Hybrid Approach.Joanna Golinska-Pilarek & Emilio Munoz Velasco - 2012 - In Emilio Corchado, Vaclav Snasel, Ajith Abraham, Michał Woźniak, Manuel Grana & Sung-Bae Cho (eds.), Hybrid Artificial Intelligent Systems. Springer. pp. 635--646.
A multimodal logic for closeness.A. Burrieza, E. Muñoz-Velasco & M. Ojeda-Aciego - 2017 - Journal of Applied Non-Classical Logics 27 (3):225-237.
Implementing a relational theorem prover for modal logic K.Angel Mora, Emilio Munoz Velasco & Joanna Golińska-Pilarek - 2011 - International Journal of Computer Mathematics 88 (9):1869-1884.


Added to PP

12 (#1,115,280)

6 months
60 (#84,286)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Joanna Golinska-Pilarek
University of Warsaw

Citations of this work

No citations found.

Add more citations