Logical consequence | EPFL Graph Search

Logical consequence (also entailment) is a fundamental concept in logic which describes the relationship between statements that hold true when one statement logically follows from one or more statements. A valid logical argument is one in which the conclusion is entailed by the premises, because the conclusion is the consequence of the premises. The philosophical analysis of logical consequence involves the questions: In what sense does a conclusion follow from its premises? and What does it mean for a conclusion to be a consequence of premises? All of philosophical logic is meant to provide accounts of the nature of logical consequence and the nature of logical truth. Logical consequence is necessary and formal, by way of examples that explain with formal proof and models of interpretation. A sentence is said to be a logical consequence of a set of sentences, for a given language, if and only if, using only logic (i.e., without regard to any personal interpretati

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 solvers to automate the verification process and to provide us with useful counterexamples when considered properties are invalid. We then enable verification in the presence of high-level Scala language features by encoding them into the dependently-typed language. We introduce an SMT-backed counterexample finding procedure which can also prove that no counterexample exists. The procedure incrementally unfolds function calls and applications in order to progressively explore the space of counterexamples. We present increasingly expressive fragments of our dependently-typed language and establish soundness and completeness properties of the procedure for each fragment. We then describe an extension which introduces support for quantifier reasoning. We discuss syntactic and semantic conditions under which the extended procedure can produce valid counterexamples in the presence of universal quantification. We present a bidirectional type checking algorithm for our dependent type system. The algorithm relies on our counterexample finding procedure to discharge verification conditions which enables predictable and effective type checking. The type system features a unified treatment of both recursive and corecursive definitions, and further admits mutual recursion between type and function definitions. We establish normalization through a sized types approach. We define a logical relation which associates a set of reducible values to each type, and then show soundness of verification by proving that evaluation of a type checked expression terminates with a reducible value. We further discuss a set of transformations which encode high-level Scala constructs into our dependently-typed language. These transformations allow our verification system to support object-oriented features such as traits and classes with multiple inheritance, as well as abstract and concrete methods with overriding. We further present a measure inference transformation which enables automated termination checking in our system. In addition to encoding language features, we discuss how Scala can be augmented with natural specification constructs and annotations that empower verification. Finally, we describe the system implementation and discuss certain practical considerations. We show that the resulting system is effective by evaluating it on a set of benchmarks and case studies comprising over 15K lines of Scala code. These benchmarks showcase both the breadth and flexibility of the system.

EPFL2019

Anterior insula reflects surprise in value-based decision-making and perception

Leyla Loued-Khenissi, Kerstin Preuschoff

The brain has been theorized to employ inferential processes to overcome the problem of uncertainty. Inference is thought to underlie neural processes, including in disparate domains such as value-based decision-making and perception. Value-based decision-making commonly involves deliberation, a time-consuming process that requires conscious consideration of decision variables. Perception, by contrast, is thought to be automatic and effortless. Both processes may call on a general neural system to resolve for uncertainty however. We addressed this question by directly comparing uncertainty signals in visual perception and an economic task using fMRI. We presented the same individuals with different versions of a bi-stable figure (Necker’s cube) and with a gambling task during fMRI acquisition. We experimentally varied uncertainty, either on perceptual state or financial outcome. We found that inferential errors indexed by a formal account of surprise in the gambling task yielded BOLD responses in the anterior insula, in line with earlier findings. Moreover, we found perceptual uncertainty and surprise in the Necker Cube task yielded similar responses in the anterior insula. These results suggest that uncertainty, irrespective of domain, correlates to a common brain region, the anterior insula. These findings provide empirical evidence that the brain interacts with its environment through inferential processes.

2020

Verified Functional Programming

Nicolas Charles Yves Voirol

EPFL2019