Robotic task planning using a backchaining theorem prover for multiplicative exponential first-order linear logic

Date

2019-11

Author

Kortik, Sitar
Saranlı, Uluç

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 United States License.

Item Usage Stats

207
views

0
downloads

In this paper, we propose an exponential multiplicative fragment of linear logic to encode and solve planning problems efficiently in STRIPS domain, that we call the Linear Planning Logic (LPL). Linear logic is a resource aware logic treating resources as single use assumptions, therefore enabling encoding and reasoning of domains with dynamic state. One of the most important examples of dynamic state domains is robotic task planning, since informational or physical states of a robot include non-monotonic characteristics. Our novel theorem prover is using the backchaining method which is suitable for logic languages like Lolli and Prolog. Additionally, we extend LPL to be able to encode non-atomic conclusions in program formulae. Following the introduction of the language, our theorem prover and its implementation, we present associated algorithmic properties through small but informative examples. Subsequently, we also present a navigation domain using the hexapod robot RHex to show LPL's operation on a real robotic planning problem. Finally, we provide comparisons of LPL with two existing linear logic theorem provers, llprover and linTAP. We show that LPL outperforms these theorem provers for planning domains.

Subject Keywords

Robotic task planning, Linear logic, Automated theorem proving, Visual navigation, Backchaining, RHex hexapod

URI

https://dx.doi.org/10.1007/s10846-018-0971-9
https://hdl.handle.net/11511/28655

Journal

Journal Of Intelligent & Robotic Systems

DOI

https://doi.org/10.1007/s10846-018-0971-9

Collections

Department of Computer Engineering, Article

Suggestions

OpenMETU
Core

Feedback motion planning of unmanned underwater vehicles via random sequential composition Ege, Emr; Orguner, Umut; Department of Electrical and Electronics Engineering (2019) In this thesis, we propose a new motion planning method to robustly and computationally efficiently solve (probabilistic) coverage, path planning, and navigation problems for unmanned underwater vehicles (UUVs). Our approach is based on synthesizing two existing methodologies: sequential decomposition of dynamic behaviors and rapidly exploring random trees. The main motivation for this integrated solution is a robust feed-back based and computationally feasible motion planning and navigation algorithm that ...
Signaling Games for Log-Concave Distributions: Number of Bins and Properties of Equilibria Kazikli, Ertan; Sarıtaş, Serkan; GEZİCİ, Sinan; Linder, Tamas; Yuksel, Serdar (2022-03-01) We investigate the equilibrium behavior for the decentralized cheap talk problem for real random variables and quadratic cost criteria in which an encoder and a decoder have misaligned objective functions. In prior work, it has been shown that the number of bins in any equilibrium has to be countable, generalizing a classical result due to Crawford and Sobel who considered sources with density supported on [0, 1]. In this paper, we first refine this result in the context of log-concave sources. For sources ...
Optimal vorticity accuracy in an efficient velocity-vorticity method for the 2D Navier-Stokes equations Akbaş, Meral; Rebholz, L. G.; Zerfas, C. (Springer Science and Business Media LLC, 2018-03-01) We study a velocity-vorticity scheme for the 2D incompressible Navier-Stokes equations, which is based on a formulation that couples the rotation form of the momentum equation with the vorticity equation, and a temporal discretization that stably decouples the system at each time step and allows for simultaneous solving of the vorticity equation and velocity-pressure system (thus if special care is taken in its implementation, the method can have no extra cost compared to common velocity-pressure schemes). ...
Numerical studies of the electronic properties of low dimensional semiconductor heterostructures Dikmen, Bora; Tomak, Mehmet; Department of Physics (2004) An efficient numerical method for solving Schrödinger's and Poisson's equations using a basis set of cubic B-splines is investigated. The method is applied to find both the wave functions and the corresponding eigenenergies of low-dimensional semiconductor structures. The computational efficiency of the method is explicitly shown by the multiresolution analysis, non-uniform grid construction and imposed boundary conditions by applying it to well-known single electron potentials. The method compares well wit...
Nonnormal regression. I. Skew distributions İslam, Muhammed Qamarul; Yildirim, F (2001-01-01) In a linear regression model of the type y = thetaX + e, it is often assumed that the random error e is normally distributed. In numerous situations, e.g., when y measures life times or reaction times, e typically has a skew distribution. We consider two important families of skew distributions, (a) Weibull with support IR: (0, infinity) on the real line, and (b) generalised logistic with support IR: (-infinity, infinity). Since the maximum likelihood estimators are intractable in these situations, we deriv...

Citation Formats

S. Kortik and U. Saranlı, “Robotic task planning using a backchaining theorem prover for multiplicative exponential first-order linear logic,” Journal Of Intelligent & Robotic Systems, pp. 179–191, 2019, Accessed: 00, 2020. [Online]. Available: https://dx.doi.org/10.1007/s10846-018-0971-9.