Workshop on Trends, Extensions, Applications and Semantics of Logic Programming

Uli Sattler: Description Logics and Ontology Languages – an introduction and overview

hbasold — Thu, 14 May 2020 20:20:25 +0000

Forum Slides

Attachments

TEASE-LP_Sattler (7 MB)

Dale Miller: Structural Proof-Theory and Logic Programming

hbasold — Thu, 14 May 2020 20:16:46 +0000

We discuss the influences of structural proof theory on logic programming and vice versa.

Forum Abstract

Attachments

Abstract Dale Miller (87 kB)

Dmitry Rozplokhas and Dmitry Boulytchev: Certified Semantics for Disequality Constraints

hbasold — Thu, 14 May 2020 12:50:17 +0000

We present an extension of our prior work on certified semantics for core miniKanren, introducing disequality constraints in the language. Semantics is parameterized by an exact definition of constraint stores, allowing us to cover different implementations. We extend our proof of search completeness to this language extension. The description and proofs are certified in Coq and a correct-by-construction interpreter is extracted.

Forum Full Abstract

Attachments

Abstract Dmitry Rozplokhas and Dmitry Boulytchev (127 kB)

Robert Zinkov, Michael Ballantyne, Gregory L. Rosenblatt and William E. Byrd: Accelerating Program Synthesis in miniKanren

hbasold — Thu, 14 May 2020 12:42:11 +0000

While many logic programming systems like miniKanren are highly expressive, they suffer from long and unpredictable running times. The challenge comes from the search algorithm being usually an uninformed search. Through the domain of program synthesis we show that it possible to greatly speedup this search by guiding it using example programs.

Forum Video Full Abstract

Attachments

Abstract Robert Zinkov, Michael Ballantyne, Gregory L. Rosenblatt and William E. Byrd (110 kB)

Marco Maggesi and Enrico Tassi: Private types in Higher Order Logic Programming

hbasold — Thu, 14 May 2020 12:40:51 +0000

We report on ongoing work on introducing a mechanism for private types in a higher-order logic programming language such as λProlog.

Forum Full Abstract

Attachments

Abstract Marco Maggesi and Enrico Tassi (124 kB)

Dmitrii Kosarev and Dmitry Boulytchev: Relational Synthesis of Pattern Matching

hbasold — Thu, 14 May 2020 12:37:25 +0000

We present an approach to pattern matching code generation based on application of relational programming and, in particular, relational interpreters.

Forum Video Full Abstract

Attachments

Abstract Dmitrii Kosarev and Dmitry Boulytchev (130 kB)

Vivek Nigam: A Proof Theory for Distributed Evidential Transactions

hbasold — Thu, 14 May 2020 12:36:33 +0000

Evidential transactions (ETs) provide auditable and composable evidence that serves as a witness or a proof that a transaction has been correctly executed by the named parties. For example, for issuing a Visa, an applicant demonstrates, among other evidence, that he has sufficient financial means to visit a foreign country. The form of evidence in ETs has traditionally been unstructured and informal, in the form of paper-based evidence. This paper proposes a formal treatment of evidence based on proof theory. In particular, we investigate the proof theory of Cyberlogic, an assertion logic for ETs, that enables the combination of evidence represented as logical derivations and as digital certificates, i.e., electronic evidence signed by a principal’s secret key. We propose a proof system for Cyberlogic, refining it with further constructions that support a wider range of ETs. We prove that the proof system admits cut-elimination.

Moreover, we propose a sound and complete focused proof system for the refinement of Cyberlogic thus enabling efficient proof-search. Furthermore, we identify a fragment of Cyberlogic, called Cyberlogic Programs, that can be used to efficiently program ETs using a variety of FOL engines. Finally, we propose Proof Certificate format for Cyberlogic Programs inspired by Foundational Proof Certificates as a means to communicate evidence and check its validity.

This is joint work with Giselle Reis, Harald Ruess, Dian Balta, Tewodros Beyene, and Natarajan Shankar.

Forum Full Abstract

Attachments

Abstract Vivek Nigam (91 kB)

Anduo Wang: Analyzing Internet Routing Policies with Answer Set Programming

hbasold — Thu, 14 May 2020 12:34:41 +0000

Internet routing is the process of selecting paths across the Internet to connect the communicating hosts, it is unique in that path selection is jointly determined by a network of independently operated networks, known as domains or Autonomous Systems (ASes), that interconnect to form the Internet. In fact, the present routing infrastructure takes such an extreme position that it favors local autonomy — an AS can use arbitrary path preference to override the default shortest path policy, at the expense of potential global oscillation — a collection of AS preferences (policies) can fail to converge on a stable path, a path that is also the most preferred possible for every AS along the path. In this paper, we examine the route oscillation problem with non-monotonic reasoning. We observe that, in the absence of any AS specific policies, Internet routing degenerates into the monotonic computation of shortest path — a preferred (shorter) (super)path always extends another preferred (sub)path; But fully autonomous AS policies are non-monotonic — a path favored by one AS can be an extension of a less preferred path of a neighbor, to which an “upgrade” to a better path can cause this AS to downgrade to a less preferred path previously discarded. Based on this insight, we present an Answer Set Programming (ASP) formulation that allows for automatic oscillation detection.

Forum Full Abstract

Attachments

Abstract Anduo Wang (134 kB)

Maria Kuklina and Ekaterina Verbitskaia: Supercompilation Strategies of Relational Programs

hbasold — Thu, 14 May 2020 12:31:08 +0000

In this paper we research methods of supercompilation in the context of relational program specialization. We implement a supercompiler for miniKanren with different unfolding strategies and compare them.

Forum Video Full Abstract

Attachments

Abstract Maria Kuklina and Ekaterina Verbitskaia (124 kB)

João Barbosa, Mário Florido and Vítor Santos Costa: Sound Type Assignment for Logic Programs

hbasold — Thu, 14 May 2020 12:30:10 +0000

Type systems are a powerful tool in modern programming languages. We argue that, to be successfully adopted by the logic programming community, the first step is to design a type system that is able to catch obvious and relevant errors at compile-time. To do so, we defined a new type system which describes polymorphic well-typings for logic programs while respecting the main properties that make types useful and semantically sound. We now tackle the question of automatically producing a well typing for a logic program. We concentrated first on the implementation of a new type inference algorithm and its application to several logic programs.

Forum Video Full Abstract

Attachments

Abstract João Barbosa, Mário Florido and Vítor Santos Costa (132 kB)