2.8k citations
- Max Planck SocietyDE261 papers
- Saarland UniversityDE124 papers
- Technische Universität BerlinDE55 papers
- Centre National de la Recherche ScientifiqueFR41 papers
- Korea UniversityKR41 papers
- Stanford UniversityUS25 papers
- Institut national de recherche en sciences et technologies du numériqueFR24 papers
- ETH ZurichCH21 papers
- Helmholtz Center for Information SecurityDE20 papers
- Technical University of MunichDE20 papers
- Université de LorraineFR17 papers
- University of LuxembourgLU16 papers
4 papers · 2 filters
The Challenge of Unifying Semantic and Syntactic Inference Restrictions
Christoph Weidenbach
While syntactic inference restrictions don't play an important role for SAT, they are an essential reasoning technique for more expressive logics, such as first-order logic, or fra…
Separateness of Variables -- A Novel Perspective on Decidable First-Order Fragments
Marco Voigt
The classical decision problem, as it is understood today, is the quest for a delineation between the decidable and the undecidable parts of first-order logic based on elegant synt…
Reconstructing veriT Proofs in Isabelle/HOL
Mathias Fleury, Hans-Jörg Schurr
Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness o…
Algebraic Invariants for Linear Hybrid Automata
Rupak Majumdar, Joël Ouaknine, Amaury Pouly +1
We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given unguarded linear hybrid automaton (i.e., a hybrid automa…