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

Kortik, Sitar
Saranlı, Uluç
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.
Journal Of Intelligent & Robotic Systems


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: