Concept
Prédicat (logique mathématique)
Publications associées (5)
Decision Procedures for Power Structures
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 ...
EPFL2023LISA – 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 ...
2023Undecidability through Fourier series
In computability theory a variety of combinatorial systems are encountered (word problems, production systems) that exhibit undecidability properties. Here we seek such structures in the realm of Analysis, more specifically in the area of Fourier Analysis. ...
Elsevier Science Bv2016Non-Clausal Satisfiability Modulo Theories
This thesis presents NC(T), an extension of the DPLL(T) scheme [16, 29] for decision procedures for quantifier-free first-order logics. In DPLL(T), a general Boolean DPLL engine is instantiated with a theory solver for the theory T. The DPLL engine is resp ...
2008A flexible motif search technique based on generalized profiles
A flexible motif search technique is presented which has two major components: (1) a generalized profile syntax serving as a motif definition languaje; and (2) a motif search method specifically adapted to the problem of finding multiple instances of a mot ...
1996