Publications associées à Complétude (logique)

Orthologic with Axioms

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

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

The completeness of the generalized eigenfunctions and an upper bound for the counting function of the transmission eigenvalue problem for Maxwell equations

Hoài-Minh Nguyên, Jean Louis-Alexandre Fornerod

Cakoni and Nguyen recently proposed very general conditions on the coefficients of Maxwell equations for which they established the discreten ess of the set of eigenvalues of the transmission problem and studied their locations. In this paper, we establish ...

2021

3D Printed Motor-Sensory Module Prototype for Facial Rehabilitation

Jamie Paik, Amir Firouzeh, Matthew Aaron Robertson

This work demonstrates the first 3D printed wearable motor-sensory module prototype designed for facial rehabilitation, focusing on facial paralysis. The novelty of the work lies in the fast fabrication of the first fully soft working prototype, including ...

MARY ANN LIEBERT, INC2022

Methodological review and detailed guidance for the life cycle interpretation phase

Xun Liao, Alexis Laurent

Life cycle interpretation is the fourth and last phase of life cycle assessment (LCA). Being a "pivot" phase linking all other phases and the conclusions and recommendations from an LCA study, it represents a challenging task for practitioners, who miss ha ...

WILEY2020

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

Generalized Incremental Model Identification for Chemical Reaction Systems

Dominique Bonvin, Julien Léo Billeter, Diogo Filipe Mateus Rodrigues, Adrien Oulevey

Identification of kinetic models and estimation of kinetic parameters in chemical reaction systems can be done using Incremental Model Identification (IMI). By using IMI, it is possible to separate the effect of the different reactions and thus investigate ...

2017

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...

Springer-Verlag Berlin2015

Implantable Multi-panel Platform for Continuous Monitoring of Exogenous and Endogenous Metabolites for Applications in Personalized Medicine

Camilla Baj-Rossi

Nowadays, scientific advances are leading to the discovery of newer, better, more targeted treatments that will improve the human health. However, despite the promising results and the major advantages in treatments offered to patients, these personalized ...

EPFL2015

Capabilities for Uniqueness and Borrowing

Martin Odersky, Philipp Haller

An important application of unique object references is safe and efficient message passing in concurrent object-oriented programming. However, to prevent the ill effects of aliasing, practical systems often severely restrict the shape of messages passed by ...

Springer2010