E-Locus - Institutional Repository of the University of Crete - Automating commonsense reasoning : a satisfiability based commonsense reasoning system incorparating a tool for measuring the SAT progress

Home Automating commonsense reasoning : a satisfiability based commonsense reasoning system incorparating a tool for measuring the SAT progress

Results - Details

[Add to Basket]

Identifier

000334361

Title

Automating commonsense reasoning : a satisfiability based commonsense reasoning system incorparating a tool for measuring the SAT progress

Alternative Title

Ένα Σύστημα Συλλογιστικής Γνώσεων Βασισμένο σε Προβλήματα Ικανοποιησιμότητας και ένα Εργαλείο για την Πρόοδο Επίλυσής τους

Author

Ταμπάκης, Ιωάννης Λεωνίδα

Thesis advisor

Πλεξουσάκης, Δημήτρης

Abstract

In recent years there has been increased use of SAT solvers for solving real-world problems in such fields as planning, model checking, and so on, by encoding the problem as a SAT instance. This is often more efficient rather than using explicit algorithms in the problem’s own domain. This thesis presents a comparison between two logical formalisms for commonsense reasoning, Situation and Event Calculus, and introduces the design and implementation of a satisfiability-based commonsense reasoning system using Event Calculus, called RES. The system takes a reasoning problem as input and produces solutions to the problem as output. It supports such reasoning types as deduction, temporal projection, abduction, planning, model checking, model finding and counterexample finding. RES supports the commonsense law of inertia, release from the commonsense law of inertia, conditional effects of events, event ramifications, events with nondeterministic effects, gradual change, triggered events, and concurrent events with cumulative or canceling effects. The SAT instances arising from real-world problems are often quite large and require hours, even days, to solve, and take up significant system resources. It would be very useful to be able to have, at any point, a measure of the progress made on solving the instance so far. In this thesis we sought to address that shortcoming with the design and implementation of a tool, called SAT-Prog to measure the progress of a SAT instance. We describe the method for incorporating SAT solvers with SAT-Prog and we present some statistics collected by using it on sample instances. Evaluation of RES on Event Calculus benchmarks problems and SAT-Prog on SAT instances, showed that Event Calculus reasoning problems can be solved efficiently using complete satisfiability solvers and SAT-Prog performs well on the majority of the cases giving us a reasonably reliable measure of solver progress.

Language

English

Issue date

2008-07-22

Collection

School/Department--School of Sciences and Engineering--Department of Computer Science--Post-graduate theses

Type of Work--Post-graduate theses

Views

489

Digital Documents
	Download document View document Views : 7