Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
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-decision procedure defined on a fragment of many-sorted first-order logic that succeeds on certain satisfiable formulas even if they contain, for example, associativity axioms. The models for which our procedure terminates have finite ranges of function symbols. We expect that our procedure can be integrated into other instantiating procedures such as E-matching with little performance impact. Our procedure is also compatible with specialized verification techniques that enable efficient reasoning about pure higher-order recursive functions. We integrated our procedure into the Leon verification framework. The implementation is publicly available and has been evaluated on non-trivial benchmarks featuring higher-order programs with quantified contracts.
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
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 ...