Publications related to Ordered Sets in the Calculus of Data Structures

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your 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

Chat with 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

Interpolation and Quantifiers in Ortholattices

Interpolation and Quantifiers in Ortholattices

Towards a secure and trustworthy imaging with non-fungible tokens

NP Satisfiability for Arrays as Powers

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

Orthologic with Axioms

Decision Procedures for Power Structures

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

On the stress tensor light-ray operator algebra

On Polynomial Algorithms for Normalizing Formulas