Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Open Access Guideline
Open Access Guideline
Postgraduate Thesis Guideline
Postgraduate Thesis Guideline
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
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
211
views
0
downloads
Cite This
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
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
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.