FroCoS Program

Here are the programs (still subject to change): FroCoS sessions will probably take place in room 118 of the Informatyka building.

FroCoS invited talks

  1. Thomas Sturm. From Complete Elimination Procedures to Subtropical Decisions over the Reals
  2. Philipp RŸmmer. Free variables and theories: revisiting rigid E-unification
  3. Andreas Herzig. Knowledge and action: how should we combine their logics?

FroCoS papers

  1. Stephan Bšhme and Marcel Lippman. Decidable Description Logics of Context with Rigid Roles
  2. Franz Baader, Gerhard Brewka, and Olivier Fernandez Gil. Adding Threshold Concepts to the Description Logic EL
  3. Stephan Borgwardt and Rafael Pen–aloza. Reasoning in Expressive Description Logics under Infinitely Valued Gšdel Semantics
  4. G‡bor Alagi and Christoph Weidenbach. NCRL-A Model Building Approach to the Bernays-Schšnfinkel Fragment
  5. Andreas Teucke and Christoph Weidenbach. First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
  6. Tobias Philipp. An Expressive Model for Instance Decomposition Based Parallel SAT Solvers
  7. Juergen Christ and Joechen Hoenicke. Weakely Equivalent Arrays
  8. Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barret. A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
  9. Maximilian Jaroscheck, Pablo Federico Dobal, and Pascal Fontaine. Adapting Real Quantifier Elimination Methods for Unsatisfiable Core Computations
  10. Francesco Alberti, Silvio Ghilardi, and Natasha Sharygina. A new Acceleration-based Combination Framework for Array Properties
  11. Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans. Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
  12. Gilles Dowek, Ying Jiang, and Guillaume Burel. A completion method to decide reachability in rewrite systems
  13. Damien Rouhling, Mahfuza Farooque, StŽphane Graham-Lengrand, Assia Mahdoubi, and Jean-Marc Notin. Axiomatic constraint systems for proof search modulo theories
  14. Sarah Winkler and RenŽ Thiemann. Formalizing Soundness and Completeness of Unravelings
  15. Nik Sultana, Christoph BenzmŸller, and Lawrence Paulson. Proofs and reconstructions
  16. Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A Rewriting Approach to the Combination of Data Structures with Bridging Theories
  17. Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, and Christophe Ringeissen. Unification and Matching in Hierarchical Combinations of Syntactic Theories
  18. Amira Zaki, Slim Abdennadher, and Thom Fruehwirth. Combining Forward and Backward Propagation
  19. Michael FŠrber and Cezary Kaliszyk. Random Forests for Premise Selection
  20. Cezary Kaliszyk, Josef Urban, and Jiri Vyskocil. Lemmatization for Stronger Reasoning in Large Theories

Tableaux papers (shared sessions with FroCoS)

  1. Christoph Wernhard. Second-Order Quantifier Elimination on Relational Monadic Formulas - A Basic Method and Some Less Expected Applications.
  2. James Brotherston, Nikos Gorogiannis. Disproving Inductive Entailments in Separation Logic via Base Pair Approximation.
  3. David Delahaye, Guillaume Bury. Integrating Simplex with Tableaux.