Publications associées à Combining Theories with Shared Set Operations

Publications associées (29)

Mechanized HOL Reasoning in Set Theory

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assum ...

2024

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

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

In Medio Stat Virtus: Combining Boolean and Pattern Matching

Giovanni De Micheli, Alessandro Tempia Calvino, Gianluca Radi

Technology mapping transforms a technology-independent representation into a technology-dependent one given a library of cells. This process is performed by means of local replacements that are extracted by matching sections of the subject graph to library ...

IEEE2024

Decision Procedures for Power Structures

Rodrigo Raya

We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction ...

EPFL2023

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

Bayes Security: A Not So Average Metric

Carmela González Troncoso, Giovanni Cherubin

Security system designers favor worst-case security metrics, such as those derived from differential privacy (DP), due to the strong guarantees they provide. On the downside, these guarantees result in a high penalty on the system's performance. In this pa ...

IEEE2023

The Impact of Data Persistence Bias on Social Media Studies

Tugrulcan Elmas

Social media studies often collect data retrospectively to analyze public opinion. Social media data may decay over time and such decay may prevent the collection of the complete dataset. As a result, the collected dataset may differ from the complete data ...

Assoc Computing Machinery2023

On algebraic array theories

Viktor Kuncak, Rodrigo Raya

Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...

Elsevier Science Inc2023

Formula Normalizations in Verification

Viktor Kuncak, Simon Guilloud, Dragana Milovancevic, 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 ...

2023

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

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

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

Three-Input Gates for Logic Synthesis

Giovanni De Micheli, Mathias Soeken, Heinz Riener, Eleonora Testa, Dewmini Sudara Marakkalage

Most logic synthesis algorithms work on graph representations of logic functions with nodes associated with arbitrary logic expressions or simple logic functions and iteratively optimize such graphs. While recent multilevel logic synthesis efforts focused ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2021

Quantification of magic angle spinning dynamic nuclear polarization NMR spectra

David Lyndon Emsley, Pierrick Berruyer, Andrea Bertarello

Dynamic nuclear polarization (DNP) allows to dramatically enhance the sensitivity of magic angle spinning nuclear magnetic resonance (MAS NMR). DNP experiments usually rely on the detection of low-γ nuclei hyperpolarized from 1H with the use of cross polar ...

Academic Press Inc - Elsevier Science2021

Quantification of Strand Accessibility in Biostable DNA Origami with Single-Staple Resolution

Maartje Martina Cornelia Bastings, Alice Comberlato

DNA-based nanostructures are actively gaining interest as tools for biomedical and therapeutic applications following the recent development of protective coating strategies prolonging structural integrity in physiological conditions. For tailored biologic ...

AMER CHEMICAL SOC2021

In-flow electrochemical detection of chemicals in droplets with pyrolysed photoresist electrodes: application as a module for quantification of microsampled dopamine

Albert René Yvon Leroy, Philippe Renaud, Arnaud Bertsch, Joan Teixidor

The electrochemical quantification of analytes in droplets of PBS separated by a fluorinated phase was investigated. PDMS-fused silica chips with pyrolysed photoresist electrodes were prepared using a simple fabrication technique and used to analyze drople ...

ROYAL SOC CHEMISTRY2021

Static and dynamic properties of non-collinear quantum antiferromagnets explored by neutron scattering

Luc Testa

This thesis is devoted to the investigation of static and dynamic properties of two different sets of quantum magnets with neutron scattering techniques and the help of linear spin wave theory. Both systems are copper-based with spin-1/2, which makes them ...

EPFL2021

Analyzing glycans cleaved from a biotherapeutic protein using a combination of ion mobility spectrometry and cryogenic ion spectroscopy

Natalia Yalovenko

The characterization of biomolecules plays a central role in biomedical research. The development of state-of-the-art technologies is needed to make such analyses faster, more sensitive, and more accurate. While mass spectrometry continues to play a centra ...

EPFL2021