Combining Theories with Shared Set Operations

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Quantification of mobility is the key to monitor the progression of mobility disorders as well as the effect of an intervention. Inertial measurement units (IMUs) with dedicated algorithms can quantify postural transitions and gait as the two key aspects o ...

Modelling and analysis of biological systems is crucial in order to quantitatively explain and predict their behaviour. The importance of modelling in systems biology becomes even more evident when tackling complex, large systems. Approaches that rely on ...

Combining Theories with Shared Set Operations

Chat with Graph Search

Mechanized HOL Reasoning in Set Theory

Orthologic with Axioms

Interpolation and Quantifiers in Ortholattices

In Medio Stat Virtus: Combining Boolean and Pattern Matching

LISA – A Modern Proof System

Bayes Security: A Not So Average Metric

The Impact of Data Persistence Bias on Social Media Studies

On algebraic array theories

Formula Normalizations in Verification

NP Satisfiability for Arrays as Powers

Scaling Language Features for Program Verification

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

Three-Input Gates for Logic Synthesis

Quantification of magic angle spinning dynamic nuclear polarization NMR spectra

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

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

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

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

Toward an objective assessment of mobility in clinical and daily activity settings

Modelling the Intracellular Environment under Uncertainty, from Post-translational Modification to Metabolic Networks