Concept

Complemented lattice

Related publications (17)

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

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 ...

Springer International Publishing Ag2024

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

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 polyno ...

Association for Computing Machinery2024

Mean value theorems for collections of lattices with a prescribed group of symmetries

Nihar Prakash Gargava

Euclidean lattices are mathematical objects of increasing interest in the fields of cryptography and error-correcting codes. This doctoral thesis is a study on high-dimensional lattices with the motivation to understand how efficient they are in terms of b ...

EPFL2024

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

Formula Normalizations in Verification

Viktor Kuncak, Simon Guilloud, Mario Bucev, Dragana Milovancevic

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 ...

2023

Packing the Boolean lattice with copies of a poset

Istvan Tomon

The Boolean lattice (2[n],subset of) is the family of all subsets of [n]={1,MIDLINE HORIZONTAL ELLIPSIS,n}, ordered by inclusion. Let P be a partially ordered set. We prove that if n is sufficiently large, then there exists a packing P of copies of P in (2 ...

WILEY2020

New Results in Integer and Lattice Programming

Christoph Hunkenschröder

An integer program (IP) is a problem of the form

\min \{f(x) : \, Ax = b, \ l \leq x \leq u, \ x \in \Z^n\}

, where

A \in \Z^{m \times n}

b \in \Z^m

l,u \in \Z^n

, and

f: \Z^n \rightarrow \Z

is a separable convex objective function. The problem o ...

EPFL2020

Almost tiling of the Boolean lattice with copies of a poset

Istvan Tomon

Let P be a partially ordered set. If the Boolean lattice (2[n],⊂) can be partitioned into copies of P for some positive integer n, then P must satisfy the following two trivial conditions: (1) the size of P is a power of 2, (2) P has a unique maximal and m ...

ELECTRONIC JOURNAL OF COMBINATORICS2018

Short Stickelberger Class Relations and Application to Ideal-SVP

Benjamin Pierre Charles Wesolowski

The worst-case hardness of finding short vectors in ideals of cyclotomic number fields (Ideal-SVP) is a central matter in lattice based cryptography. Assuming the worst-case hardness of Ideal-SVP allows to prove the Ring-LWE and Ring-SIS assumptions, and t ...

Springer International Publishing Ag2017

New Results in Integer and Lattice Programming

Christoph Hunkenschröder

An integer program (IP) is a problem of the form

\min \{f(x) : \, Ax = b, \ l \leq x \leq u, \ x \in \Z^n\}

, where

A \in \Z^{m \times n}

b \in \Z^m

l,u \in \Z^n

, and

f: \Z^n \rightarrow \Z

is a separable convex objective function. The problem o ...

EPFL2020