LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers.

*(English)*Zbl 1398.68026
EPiC Series in Computing 46. Manchester: EasyChair. 522 p., open access (2017).

**
Show indexed articles as search result.
**

Following the call for papers, LPAR-21 received 68 abstracts, materializing into 54 submissions. Each submission was reviewed by a panel of 48 Program Committee (PC) members. The PC was assisted by 47 additional reviewers and decided to accept 30 papers. In addition to the presentation of these regular papers, LPAR-21 included the following invited talks:

– Rupak Majumdar (Max Planck Institute for Software Systems, Germany): Programming by Composing Filters

– Stephen Muggleton (Imperial College London, United Kingdom): Meta-Interpretive Learning of Logic Programs

– Willem Visser (Stellenbosch University, South Africa): Probabilistic Symbolic Execution: A New Hammer

as well as seven short talks presenting further papers.

The EasyChair system provided an indispensible platform for all matters related to the reviewing process, production of these proceedings, program and web page generation, and registration of participants.

Collocated with LPAR-21 was the 12th International Workshop on the Implementation of Logics (IWIL), organized by Stephan Schulz, Geoff Sutcliffe, and Josef Urban.

The local conference organisation was done by Geoff Sutcliffe.

The articles of mathematical interest will be reviewed individually. For the preceding conference see [Zbl 1326.68013].

Indexed articles:

Fischer, Jeffrey M.; Majumdar, Rupak, Programming by composing filters, 1-13 [Zbl 1403.68023]

Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph, Theorem provers for every normal modal logic, 14-30 [Zbl 1403.68225]

Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef, TacticToe: learning to reason with HOL4 tactics, 15-143 [Zbl 1403.68224]

Kiesl, Benjamin; Suda, Martin; Seidl, Martina; Tompits, Hans; Biere, Armin, Blocked clauses in first-order logic, 31-48 [Zbl 1403.68240]

Kovács, Laura; Voronkov, Andrei, First-order interpolation and interpolating proof systems, 49-64 [Zbl 1402.03041]

Philipp, Tobias; Rebola-Pardo, Adrián, Towards a semantics of unsatisfiability proofs with inprocessing, 65-84 [Zbl 1403.68244]

Loos, Sarah; Irving, Geoffrey; Szegedy, Christian; Kaliszyk, Cezary, Deep network guided proof search, 85-105 [Zbl 1403.68197]

Kahramanoğulları, Ozan, Deep proof search in MELL, 106-124 [Zbl 1402.03089]

Bourbouh, Hamza; Garoche, Pierre-Loic; Garion, Christophe; Gurfinkel, Arie; Kahsai, Temesghen; Thirioux, Xavier, Automated analysis of Stateflow models, 144-161 [Zbl 1403.68122]

Bauer, Sabine; Hofmann, Martin, Decidable linear list constraints, 181-199 [Zbl 1403.68232]

Filho, Dimas Melo; Freitas, Fred; Otten, Jens, RACCOON: a connection reasoner for the description logic \(\mathcal{ALC}\), 200-211 [Zbl 1403.68262]

Hannula, Miika; Kontinen, Juha; Link, Sebastian, On the interaction of inclusion dependencies with independence atoms, 212-226 [Zbl 1403.68053]

Bogaerts, Bart; Ternovska, Eugenia; Mitchell, David, Propagators and solvers for the algebra of modular systems, 227-248 [Zbl 1403.68279]

Frohn, Florian; Giesl, Jürgen, Analyzing runtime complexity via innermost runtime complexity, 249-268 [Zbl 1403.68106]

Hainry, Emmanuel; Péchoux, Romain, Higher order interpretation for higher order complexity, 269-285 [Zbl 1403.68032]

Boumarafi, Yazid M.; Sais, Lakhdar; Salhi, Yakoub, From SAT to maximum independent set: a new approach to characterize tractable classes, 286-299 [Zbl 1403.68073]

Echahed, Rachid; Maignan, Aude, Parallel graph rewriting with overlapping rules, 300-318 [Zbl 1403.68104]

Bistarelli, Stefano; Martinelli, Fabio; Matteucci, Ilaria; Santini, Francesco, A quantitative partial model-checking function and its optimisation, 319-337 [Zbl 1403.68121]

Mordvinov, Dmitry; Fedyukovich, Grigory, Synchronizing constrained Horn clauses, 338-355 [Zbl 1403.68243]

Kahsai, Temesghen; Kersten, Rody; Rümmer, Philipp; Schäf, Martin, Quantified heap invariants for object-oriented programs, 368-384 [Zbl 1403.68126]

Barthe, Gilles; Espitau, Thomas; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves, Proving uniformity and independence by self-composition and coupling, 385-403 [Zbl 1403.68140]

Baaz, Matthias; Preining, Norbert, Gödel logics and the fully boxed fragment of FO-LTL, 404-416 [Zbl 1402.03025]

Ciabattoni, Agta; Ramanayake, Revantha, Bunched hypersequent calculi for distributive substructural logics, 417-434 [Zbl 1402.03029]

Lellmann, Björn; Olarte, Carlos; Pimentel, Elaine, A uniform framework for substructural logics with modalities, 435-455 [Zbl 1402.03030]

Gigante, Nicola; Montanari, Angelo; Reynolds, Mark, A one-pass tree-shaped tableau for LTL+past, 456-473 [Zbl 1402.03026]

Jouannaud, Jean-Pierre; Strub, Pierre-Yves, Coq without type casts: a complete proof of Coq Modulo Theory, 474-489 [Zbl 1403.68227]

Taqdees, Syeda Hira; Klein, Gerwin, Reasoning about translation lookaside buffers, 490-508 [Zbl 1403.68037]

Cruz-Filipe, Luís; Schneider-Kamp, Peter, Formally proving the Boolean Pythagorean triples conjecture, 509-522 [Zbl 1403.68222]

##### MSC:

68-06 | Proceedings, conferences, collections, etc. pertaining to computer science |

03-06 | Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations |

03B70 | Logic in computer science |

68T27 | Logic in artificial intelligence |

00B25 | Proceedings of conferences of miscellaneous specific interest |