Concept

Horn clause

Related publications (9)

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.

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

2024

On recursion-free Horn clauses and Craig interpolation

Viktor Kuncak, Hossein Hojjat

One of the main challenges in software verification is efficient and precise analysis of programs with procedures and loops. Interpolation methods remain among the most promising techniques for such verification. To accommodate the demands of various progr ...

Springer2015

Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. Quantifier instantiation combined with ground decision procedure alone is insufficient to prove many formulas ...

Springer-Verlag Berlin2015

On Induction for SMT Solvers

Viktor Kuncak, Andrew Joseph Reynolds

2014

On Complete Reasoning about Axiomatic Specifications

Viktor Kuncak, Swen Jacobs

Automated software verification tools typically accept specifications of functions in terms of pre- and postconditions. However, many properties of functional programs can be more naturally specified using a more general form of universally quantified prop ...

2010

Approximate Confidence Computation in Probabilistic Databases.

Christoph Koch

This paper introduces a deterministic approximation algorithm with error guarantees for computing the probability of propositional formulas over discrete random variables. The algorithm is based on an incremental compilation of formulas into decision diagr ...

2010

Functional dependencies in OWL ABoxes

Jean Paul Calbimonte Perez

Functional Dependency (FD) has been extensively studied in database theory. Most recently there have been some works investigating the implications of extending Description Logics with functional dependencies. In particular the OWL ontology language offers ...

2009

Functional Dependency has been extensively studied in database theory. It provides an elegant formalism for specifying key constraints and is the basis for normalization theory used in Relational database design. Given its known axiomatization through logi ...

2007

Coordinating Agile Systems through the Model-based Execution of Temporal Plans

Thomas Léauté

Agile autonomous systems are emerging, such as unmanned aerial vehicles (UAVs), that must robustly perform tightly coordinated time-critical missions; for example, military surveillance or search-and-rescue scenarios. In the space domain, execution of temp ...

Massachusetts Institute of Technology (MIT)2005