Concept

Higher-order logic

Related publications (32)

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

2023

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

Positive Definite Completions and Continuous Graphical Models

Kartik Waghmare

This thesis concerns the theory of positive-definite completions and its mutually beneficial connections to the statistics of function-valued or continuously-indexed random processes, better known as functional data analysis. In particular, it dwells upon ...

EPFL2023

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

A template for constructing Bayesian networks in forensic biology cases when considering activity level propositions

Christophe Champod, Alex Biedermann

The hierarchy of propositions has been accepted amongst the forensic science community for some time. It is also accepted that the higher up the hierarchy the propositions are, against which the scientist are competent to evaluate their results, the more d ...

ELSEVIER IRELAND LTD2018

Adaptive WENO methods based on radial basis functions reconstruction

Jan Sickmann Hesthaven, Caterina Bigoni

We explore the use of radial basis functions (RBF) in the weighted essentially non-oscillatory (WENO) reconstruction process used to solve hyperbolic conservation laws, resulting in a numerical method of arbitrarily high order to solve problems with discon ...

Springer Verlag2017

On Satisfiability for Quantified Formulas in Instantiation-Based Procedures

Viktor Kuncak, Nicolas Charles Yves Voirol

Procedures for first-order logic with equality are used in many modern theorem provers and solvers, yet procedure termination in case of interesting sub-classes of satisfiable formulas remains a challenging problem. We present an instantiation-based semi-d ...

2016

Automating Verification of Functional Programs with Quantified Invariants

Viktor Kuncak, Nicolas Charles Yves Voirol

We present the foundations of a verifier for higher-order functional programs with generics and recursive algebraic data types. Our ver- ifier supports finding sound proofs and counterexamples even in the presence of certain quantified invariants and recur ...

2016

A Polynomial Regularity Lemma For Semialgebraic Hypergraphs And Its Applications In Geometry And Property Testing

János Pach

In this paper, we prove several extremal results for geometrically defined hypergraphs. In particular, we establish an improved lower bound, single exponentially decreasing in k, on the best constant delta > 0 such that the vertex classes P-1,...,P-k of ev ...

Society for Industrial and Applied Mathematics2016

On Counter-Example Complete Verification for Higher-Order Functions

Viktor Kuncak, Etienne Kneuss, Nicolas Charles Yves Voirol

We present a verification procedure for pure higher-order functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counter-examples. The procedure reduces the analysis of higher-orde ...

2015

Graph Chatbot

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.