LPAR 2024: 25TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING
PROGRAM FOR TUESDAY, MAY 28TH
Days:
previous day
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 8

Invited talk

Chair:
Nikolaj Bjørner (Microsoft, United States)
Location: Master Class
09:00
Erika Abraham (RWTH Aachen, Germany)
On the Idea of Exploration-guided Satisfiability Checking

ABSTRACT. Satisfiability checking is a research area devoted to the development and implementation of algorithms for the automated satisfiability check of logical formulas. SAT solving for propositional logic became impressively powerful due to an elegant combination of a smart search space exploration and proof construction. This idea has been later generalized to quantifier-free first-order logic formulas over some theories, most notably quantifier-free real algebra, in the framework of the model constructing satisfiability calculus (MCSAT). Both approaches are based on the generalization of "wrong guesses" made by the exploration into pieces of a proof, which are collected and used to synthesize a global proof during the solving process. While being one of the currently best approaches, for large or complex formulas, a large number of "proof pieces" cause high effort for their processing and thus restrict scalability. Thus the question comes up whether there are ways to store such information in a more structured way, which requires lower costs for processing. This thought is taken up by the method of the cylindrical algebraic coverings, developed for the satisfiability check of conjunctions of polynomial constraints. In this talk, we will discuss the above ideas and methods, and highlight their relations and differences.

10:30-12:30 Session 9

Theories and Logics

Chair:
Delia Kesner (Université Paris Cité, France)
Location: Master Class
10:30
Johannes Schoisswohl (TU Wien, Austria)
Laura Kovács (TU Wien, Austria)
Konstantin Korovin (The University of Manchester, UK)
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

ABSTRACT. We introduce Virtual Integer-Real Arithmetic Substitution (VIRAS), a quantifier elimination procedure for deciding quantified linear mixed integer-real arithmetic problems. VIRAS combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that VIRAS gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve.

11:00
Guilherme Toledo (Bar Ilan University, Israel)
Yoni Zohar (Bar-Ilan University, Israel)
Combining Combination Properties: Minimal Models

ABSTRACT. This is part of an ongoing research project, with the aim of studying the connections between model-theoretic properties related to theory combination in Satisfiability Modulo Theories. In previous work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessibility, strong finite witnessibility, the finite model property, and stable finiteness.

The first two properties are needed for Nelson-Oppen combination, the third and fourth are related to polite combination, the third and fifth correspond to strong politeness, and the last two are related to the combination of shiny theories.

However, the remaining key property of shiny theories, namely, the ability to compute the cardinalities of minimal models, was not yet analyzed. In this paper we study this property.

11:30
Mark Chimes (TU Wien, Austria)
Radu Iosif (Verimag, CNRS, University of Grenoble Alpes, France)
Florian Zuleger (TU Wien, Austria)
Tree-Verifiable Graph Grammars

ABSTRACT. Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While for words and trees syntactic grammar restrictions are known that guarantee that the associated languages of words resp. trees are regular - and hence, MSO definable - the situation is more complicated for graphs. Here, Courcelle proposed the notion of regular graph grammars, a syntactic restriction of HR grammars that guarantees the definability of the associated languages of graphs in Counting Monadic Second Order Logic (CMSO). However, these grammars are not complete in the sense that not every CMSO definable set of graphs of bounded tree-width can be generated by a regular graph grammar. In this paper, we introduce a new syntactic restriction of HR grammars, called tree-verifiable graph grammars, and a new notion of bounded tree-width, called embeddable bounded tree-width, where the later restricts the trees of a tree-decomposition to be a subgraph of the analyzed graph. The main property of tree-verifiable graph grammars is that their associated languages are CMSO definable and that the have bounded embeddable tree-width. We show further that they strictly generalize the regular graph grammars of Courcelle. Finally, we establish a completeness result, showing that every language of graphs that is CMSO definable and of bounded embeddable tree-width can be generated by a tree-verifiable graph grammar.

12:00
Matthias Lanzinger (TU Wien, Austria)
Stefano Sferrazza (University of Oxford, UK)
Przemysław Andrzej Wałęga (University of Oxford, UK)
Georg Gottlob (University of Calabria, Italy)
Fuzzy Datalog$^\exists$ over Arbitrary t-norms

ABSTRACT. One of the main challenges in the area of Neuro-symbolic AI is to perform logical reasoning in the presence of neural and symbolic datasets. This requires the combination of heterogeneous data sources such as knowledge graphs, neural model predictions, structured databases, crowd-sourced data, and many more. In this paper we introduce $t$-Datalog$^\exists$ as a formalism for such reasoning tasks, $t$-Datalog$^\exists$ generalises of Datalog with existential rules or Datalog$^\exists$ (also commonly referred to as tuple-generating dependencies) by allowing the use of arbitrary t-norms in place of classical conjunction in rule bodies. The resulting formalism combines the best of both worlds. It extends the power and flexibility of Datalog$^\exists$ to neuro-symbolic reasoning tasks while preserving many of the desirable properties of the classical case. In particular, we show that natural extensions of the chase to our setting produces \emph{fuzzy universal models}, and that the complexity of reasoning in important decidable fragments remains the same as in the classical setting.

14:30-16:00 Session 10

Proof Theory

Chair:
Matthias Baaz (Technische Universit"at Wien, Austria)
Location: Master Class
14:30
Pablo Barenbaum (Universidad Nacional de Quilmes (CONICET) and ICC, Universidad de Buenos Aires, Argentina)
Delia Kesner (Université Paris Cité, France)
Mariana Milicich (Université Paris Cité, France)
Hybrid Intersection Types for PCF

ABSTRACT. Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together without making use of an encoding into a common target framework. This work proposes an intersection type system for PCF with a specific notion of evaluation, called PCFH. Although this form of evaluation is sometimes referred to as “call-by-value”, evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV-like operational behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only that typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the normalization sequences to normal form. This type system is then refined to a tight one, offering exact information regarding the length of normalization sequences.

15:00
Giulio Guerrieri (University of Sussex, UK)
Giulia Manara (Roma Tre and Paris Cité, IRIF, France)
Lorenzo Tortora de Falco (Università Roma Tre, Italy)
Lionel Vaux Auclair (Aix Marseille Université, France)
Confluence for Proof-Nets via Parallel Cut Elimination

ABSTRACT. We provide the first proof of confluence for cut elimination in multiplicative-exponential linear logic proof-nets that is not based on Newman's lemma or strong normalization, not even indirectly. To achieve our goal, we take inspiration from Tait and Martin-Lof's method based on parallel reduction for the lambda-calculus, even though the wilder realm of untyped proof-nets makes the proof subtler and more challenging.

15:30
Ozan Kahramanogullari (Free University of Bozen-Bolzano, Italy)
Deep Inference in Proof Search: The Need for Shallow Inference

ABSTRACT. Deep inference is a proof theoretical formalism that generalises the “shallow inference” of the sequent calculus by permitting the application of inference rules like term rewriting rules. Deep inference makes it possible to access shorter proofs than sequent calculus; however, with the cost of increased nondeterminism, an obstacle in front of proof search applications. Deep inference is essential for designing system BV, an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. MLL has shallow inference systems, whereas BV is impossible with a shallow-only system. As Tiu showed, any restriction on rule depth makes a system incomplete for BV. This paper shows that any restriction that rules out shallow rules makes the system incomplete, too. Our results indicate that for system BV, shallow and deep rules must coexist for completeness. We provide extensive empirical evidence that deep inference can still be faster than shallow inference when used strategically with a proof theoretical technique for reducing nondeterminism. We show that prioritising deeper rule instances reduces the cost of proof search by reducing the size of the managed contexts, consequently providing more immediate access to shorter proofs. Moreover, we identify a class of MLL formulae with deep inference proof search times that grow linearly in the number of atoms in contrast to an exponential growth pattern with shallow inference. We introduce a large and exhaustive benchmark for MLL, with and without mix, and a proof search framework to apply various search strategies, which should be of independent interest.

16:30-18:00 Session 11: Local Participants Active Research
Chair:
Geoff Sutcliffe (University of Miami, United States)
Location: Master Class
16:30
Prakash Seewoosunkur (Financial Services Commission Mauritius, Mauritius)
The Application of Artificial Intelligence in the Financial Services Sector - Risks and Opportunities

ABSTRACT. TBA

16:40
Suraj Juddoo (Mauritius Digital Promotion Agency, Mauritius)
Mauritius as a Burgeoning AI Hub and Way Forward

ABSTRACT. TBA

16:50
Maleika Heenaye-Mamode Khan (University of Mauritius, Mauritius)
The Potential and Future of AI in the Medical Field

ABSTRACT. TBA

17:20
Quentin Adam (Mantu, Mauritius)
From Sugar Cane Fields to Cybercities: Data Science Bridging the Gap in Healthcare Access

ABSTRACT. I will explore the unique challenges and transformative opportunities within the field of Data Science in Mauritius, emphasizing its potential to enhance basic healthcare access both locally and globally. My experience and insights are deeply rooted in my personal and professional journey, which remains anchored in the Mauritian sand. Born and raised in Mauritius, my professional journey in human biology, health, and data science has spanned continents, from the University of Western Australia to tech hubs in the U.S. Despite global engagements, my focus remains on Mauritius - a microcosm reflecting the complex health challenges of nearly 1 billion people from the Indian subcontinent and Africa. This unique demographic mix, evolving from sugar cane fields to cybercities, highlights our rapid innovation and adaptability. However, it also underscores the pressing need to address escalating public health disparities, leveraging our nimble environment where even small innovations can lead to disproportionately large impacts.

17:40
David Koon (Chinese Business Chamber, Mauritius)
Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business

ABSTRACT. Internship Opportunities in Mauritius, and Real-world Examples of AI Implementation in Business