PADL 2023
who it's for
answer set programmers, logic programmers, knowledge representation researchers, language designers and compiler developers, formal methods engineers, program analysis and verification engineers, research software engineers
topics
answer set programming optimizations; incremental ASP evaluation; hybrid knowledge bases for OWL 2 QL; logic DSLs targeting P4; datalog incremental rollback; constrained Horn clause satisfiability; functional logic compilation (Curry); hygienic macro expansion (Racket); program synthesis by example propagation; execution time verification with tight bounds; provenance-based rollback with ILP; scheduling with hybrid ASP and SMT
| title | author | length |
|---|---|---|
| Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL | Haya Majid Qureshi, Wolfgang Faber | 58m |
Claims that MSER entailment over OWL 2 QL can be handled by Hybrid Knowledge Bases through a pair of translations: one that keeps the original metamodeling… | ||
| Fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (App... | Birthe van den Berg, Tom Schrijvers, Peter Dedecker | 28m |
A Haskell-based DSL called Fluo DSL in Haskell executes lists of measurement elements (irradiation, camera triggers, waits) and nests them with stage loops and… | ||
| SwitchLog: A Logic Programming Language for Network Switches | Vaibhav Mehta, Devon Loehr, John Sonchack, David Walker | 29m |
Introduces a restricted logic DSL that compiles to Lucid then P4 and targets Intel Tofino; programs use key-value tables with per-key merge operators (min… | ||
| Formalizing and Reasoning about Contracts between Agents | Dylan Flynn, Chasity Nadeau, Jeannine Shantz, Marcello Balduccini, Tran Cao Son, Edward Griffor | 31m |
Proposes LC, an extension of action language B that encodes contracts as public clauses plus private mappings to requirements from the NIST CPS concern tree… | ||
| Jury-trial Story Construction and Analysis using Goal-directed Answer Set Progra... | Zesheng Xu, Gopal Gupta, Elmer Salazar, Joaquín Arias, Sarat Chandra Varanasi | 30m |
Goal-directed Answer Set Programming with s(CASP) top-down ASP models Commonwealth of Massachusetts v. Johnson as facts and defaults, then queries for… | ||
| Solving Vehicle Equipment Specification Problems with Answer Set Programming | Raito Takeuchi, Mutsunori Banbara, Naoyuki Tamura, Torsten Schaub | 28m |
System named aspcafe converts OVF instances into ASP facts and solves mono- and multi-objective CAFE problems using clingo and asprin. Basic encoding models… | ||
| Pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance ... | Anssi Yli-Jyrä, Masood Feyzbakhsh Rankooh, Tomi Janhunen | 33m |
Defines miscoverage as the optimization objective for preventive maintenance, gives six concrete pruning constraints that identify prunable schedules (lagging… | ||
| Integrating ASP-based incremental reasoning in the videogame development workflo... | Denise Angilica, Giovambattista Ianni, Francesco Pacenza, Jessica Zangari | 28m |
Integration of Incremental-DLV2 into ThinkEngine for Unity wires a live, multi-shot ASP solver to reactive and planning NPC modules and three game benchmarks… | ||
| UAV Compliance Checking using Answer Set Programming and Minimal Explanations to... | Sarat Chandra Varanasi, Baoluo Meng, Christopher Alexander, Szabolcs Borgyos | 24m |
Implements an ASP-based compliance checker for AMA Safety Code rules, adds a new algorithm that computes minimal explanations for violating rules by treating… | ||
| Flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybrid Answer ... | Ramsha Ali, Mohammed M. S. El-Kholany, Martin Gebser | 29m |
A hybrid Answer Set Programming model using difference logic encodes machine processing, setup + maintenance windows and flexible assignment of operations to… | ||
| Modern Macros | Robby Findler | 01h 03m |
Racket treats macros as an open front end to the compiler: the expander handles three concrete cases—macro call, macro definition (define-syntax), and core… | ||
| Automatic Rollback Suggestions for Incremental Datalog Evaluation | David Zhao, Pavle Subotic, Mukund Raghothaman, Bernhard Scholz | 26m |
A debugging method computes incremental provenance to identify which inserted or deleted Datalog input tuples enable each error derivation, encodes the minimal… | ||
| RICE: An Optimizing Curry Compiler | Steven Libby | 30m |
RICE is written entirely in Curry and turns Curry source into a C backend via an imperative IL called ICurry, using AST-to-AST transformations (fixed‑point… | ||
| Embedding Functional Logic Programming in Haskell via a Compiler Plugin | Kai-Oliver Prott, Finn Teegen, Jan Christiansen | 31m |
Claims an embedding of a functional-logic language into Haskell by a GHC plugin that performs a monadic lifting transformation after typechecking, preserving… | ||
| Program Synthesis Using Example Propagation | Niek Mulleners, Johan Jeuring, Bastiaan Heeren | 26m |
Scrybe is an example-based synthesizer for a statically typed functional language that combines top-down deductive search (λ2 style) with Smyth-style live… | ||
| Execution Time Program Verification With Tight Bounds | Ana Carolina Silva, Manuel Barbosa, Mario Florido | 22m |
Proof system gives three Hoare-style logics with worst-case bounds, amortized potential method, and an exact-cost logic (language restricted: equal-cost… | ||
| From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriti... | Misaki Kojima, Naoki Nishida | 25m |
Extends LC term rewrite systems to reduce starvation freedom to an all-path reachability (APR) check by instrumenting states with a counter C with… | ||
| Multiple Query Satisfiability of Constrained Horn Clauses | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti | 31m |
A sound and complete equisatisfiable transformation rewrites a CHC set with multiple queries so each output query incorporates constraints from the others… | ||
| Dynamic slicing of Reaction Systems based on assertions and monitors | Linda Brodo, Roberto Bruni, Moreno Falaschi | 29m |
First dynamic slicer for Reaction Systems that prunes past computation steps to expose exactly which reactions and entities cause a chosen subset, implemented… | ||
| Linear Algebraic Abduction with Partial Evaluation | Tuan Nguyen, Katsumi Inoue, Chiaki Sakama | 31m |
Recasts propositional Horn abduction as matrix operations and applies partial evaluation (unfolding via powers of a reductive program matrix) to collapse… | ||
| Towards Declarative Content Generation for Creativity Support Tools | Chris Martens | 58m |
Argues that answer set programming (ASP) can specify generative spaces for game/art content but has practical gaps: uses clingo to generate tile‑map heightmaps… | ||
| nothing matches | ||