Logic for Programming, Artificial Intelligence, and Reasoning: 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, ProceedingsMartin Davis, Ansgar Fehnker, Annabelle McIver, Andrei Voronkov This book constitutes the proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-20, held in November 2015, in Suva, Fiji.
The 43 regular papers presented together with 1 invited talk included in this volume were carefully reviewed and selected from 92 submissions. The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. |
Contents
| 1 | |
| 16 | |
| 31 | |
On Antisubsumptive Knowledge Enforcement | 48 |
Value Sensitivity and Observable Abstract Values for Information Flow Control | 63 |
SATBased Minimization of Deterministic Automata | 79 |
Fairly Efficient Machine Learning Connection Prover | 88 |
Decidability Introduction Rules and Automata | 97 |
Fine Grained SMT Proofs for the Theory of FixedWidth BitVectors | 340 |
Abstract Domains and Solvers for Sets Reasoning | 356 |
Sharing HOL4 and HOL Light Proof Knowledge | 372 |
Relational Reasoning via Probabilistic Coupling | 387 |
A Contextual Logical Framework | 402 |
Enhancing SearchBased QBF Solving by Dynamic Blocked Clause Elimination | 418 |
Reasoning About Loops Using Vampire in KeY | 434 |
Compositional Propositional Proofs | 444 |
Analyzing Internet Routing Security Using Model Checking | 112 |
Boolean Formulas for the Static Identification of Injection Attacks in Java | 130 |
An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials | 146 |
Controller Synthesis for MDPs and Frequency LTL | 162 |
Automated Benchmarking of Incremental SAT and QBF Solvers | 178 |
A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic | 187 |
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs | 203 |
Tools for Inductive Provers | 219 |
Verification of Concurrent Programs Using Trace Abstraction Refinement | 233 |
Synchronized Recursive Timed Automata | 249 |
Focused Labeled Proof Systems for Modal Logic | 266 |
On CTL with Graded Path Modalities | 281 |
On Subexponentials Synthetic Connectives and Multilevel Delimited Control | 297 |
On the Expressive Power of Communication Primitives in Parameterised Systems | 313 |
There Is No Best Normalization Strategy for HigherOrder Reasoners | 329 |
Fast Embeddable Prolog Interpreter | 460 |
Normalisation by Completeness with Heyting Algebras | 469 |
Using Program Synthesis for Program Analysis | 483 |
Finding Inconsistencies in Programs with Loops | 499 |
Modular Multiset Rewriting | 515 |
Modelling Moral Reasoning and Ethical Responsibility with Logic Programming | 532 |
Constrained Term Rewriting tooL | 549 |
Proof Search in Nested Sequent Calculi | 558 |
TableauBased Revision over SHIQ TBoxes | 575 |
Gamifying Program Analysis | 591 |
Automated Discovery of Simulation Between Programs | 606 |
SAT Modulo Intuitionistic Implications | 622 |
| 638 | |
Other editions - View all
Common terms and phrases
abstract abstract interpretation algorithm analysis applied approach assignment atoms attacker automata automaton axiom benchmarks bigraph Boolean complete Comput constraints construction context crowdsourcing cube defined Definition denote derivation domain dynamic encoding equivalent evaluation example extended finite first-order focused formula fragment function GCTL Heidelberg Heidelberg 2015 HOL Light Horn clause implementation induction input introduced introduction rules intuitionistic intuitionistic logic invariants iteration label language Lemma linear logic LNCS loop modal logic model checking MT(O multiset Natural Deduction nested sequent node ontology operator partial order reduction path predicate problem proof system properties propositional prove QBCE QCDCL quantified reachability reduction relation SAT solvers satisfiable Sect semantics sequent calculus simulation Skolemization solving Springer strategy sub(O subexponentials subset symbols term Theorem theory tool transition valid valuation variables verification