Concept

Automated reasoning

Related publications (90)

MDD propagators with explanation

Multi-valued decision diagrams (MDDs) are a convenient approach to representing many kinds of constraints including table constraints, regular constraints, complex set and multiset constraints, as well as ad-hoc problem specific constraints. This paper int ...

2011

The Accuracy of Automatic Photogrammetric Techniques on Ultra-light UAV Imagery

Pascal Fua, Dario Floreano, Jean-Christophe Zufferey, Antoine Beyeler, Christoph Strecha, Olivier Küng, François Gervaix

This paper presents an affordable, fully automated and accurate mapping solutions based on ultra-light UAV imagery. Several datasets are analysed and their accuracy is estimated. We show that the accuracy highly depends on the ground resolution (flying hei ...

2011

MUNCH - Automated Reasoner for Sets and Multisets

Viktor Kuncak, Ruzica Piskac

This system description provides an overview of the MUNCH reasoner for sets and multisets. MUNCH takes as the input a formula in a logic that supports expressions about sets, multisets, and integers. Constraints over collections and integers are connected ...

Springer2010

In defense of large qualitative calculi

Jingshi Li

The next challenge in qualitative spatial and temporal reasoning is to develop calculi that deal with different aspects of space and time. One approach to achieve this is to combine existing calculi that cover the different aspects. This, however, can lead ...

2010

Reasoning with large ontologies stored in relational databases: The OntoMinD approach

Stefano Spaccapietra, Christine Parent

A major obstacle to the development of ontologies in support of the Semantic Web is the poor capability of current ontology techniques to handle very large ontologies, in particular regarding scalability of reasoners. This paper builds on the assumption th ...

2010

On Locality of One-Variable Axioms and Piecewise Combinations

Viktor Kuncak, Swen Jacobs

Local theory extensions provide a complete and efficient way for reasoning about satisfiability of certain kinds of universally quantified formulas modulo a background theory. They are therefore useful in automated reasoning, software verification, and syn ...

2010

Counterexample-Guided Focus

The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right ...

2010

A Fully Automated Approach to Segmentation of Irregularly Shaped Cellular Structures in EM Images

Pascal Fua, Radhakrishna Achanta, Vincent Lepetit, Kevin Smith, Aurélien Lucchi

While there has been substantial progress in segmenting natural im-ages, state-of-the-art methods that perform well in such tasks unfortunately tend to underperform when confronted with the different challenges posed by electron microscope (EM) data. For e ...

Springer2010

ASSET: A robust algorithm for the automated segmentation and standardization of early Caenorhabditis elegans embryos

Pierre Gönczy, Felix Naef, Simon Blanchoud, Yemima Suryani Budirahardja

The early Caenorhabditis elegans embryo is an attractive model to investigate evolutionarily conserved cellular mechanisms. However, there is a paucity of automated methods to gather quantitative information with subcellular precision in this system. We de ...

Wiley-Blackwell2010

On Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas ...

2009

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.