Publications associées à Ordered Sets in the Calculus of Data Structures

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Cham2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having po ...

On Polynomial Algorithms for Normalizing Formulas

Viktor Kuncak, Simon Guilloud, Mario Bucev

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

2022

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

Viktor Kuncak, Simon Guilloud

We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomo ...

Springer2022

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...

Springer, Cham2022

Towards a secure and trustworthy imaging with non-fungible tokens

Touradj Ebrahimi, Evgeniy Upenik, Davi Nachtigall Lazzarotto

Non fungible tokens (NFTs) are used to define the ownership of digital assets. More recently, there has been a surge of platforms to auction digital art as well as other digital assets in form of image, video, and audio content of all sorts. Although NFTs ...

2021

Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma

Friedrich Eisenbrand

We consider integer programming problems in standard form max{c(T)x : Ax = b, x >= 0, x is an element of Z(n)} where A is an element of Z(mxn), b is an element of Z(m), and c is an element of Z(n). We show that such an integer program can be solved in time ...

ASSOC COMPUTING MACHINERY2020

Ordered Sets in the Calculus of Data Structures

Graph Chatbot

Chattez avec Graph Search

Interpolation and Quantifiers in Ortholattices

Interpolation and Quantifiers in Ortholattices

Orthologic with Axioms

Decision Procedures for Power Structures

On Polynomial Algorithms for Normalizing Formulas

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

NP Satisfiability for Arrays as Powers

Towards a secure and trustworthy imaging with non-fungible tokens

On the stress tensor light-ray operator algebra

Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma

Decision Procedures for Power Structures

On Polynomial Algorithms for Normalizing Formulas

Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma

Interpolation and Quantifiers in Ortholattices

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

Interpolation and Quantifiers in Ortholattices

Orthologic with Axioms

Towards a secure and trustworthy imaging with non-fungible tokens

On the stress tensor light-ray operator algebra

NP Satisfiability for Arrays as Powers