FroCoS 2015

Lecture Room 118A/B
Instytut Informatyki
Ulica Joliot Curie 15, Wrocław, Poland

Monday, September 21

  12:30–13:55 Lunch
  13:55–14:00 (Shared with TABLEAUX) Start of FroCoS and TABLEAUX
    Hans de Nivelle (Conference Chair)
  14:00–15:30 (Shared with TABLEAUX) Session 11 (Chair: Hans de Nivelle)
  14:00 Invited Talk: From Complete Elimination Procedures to Subtropical Decisions over the Reals
    Thomas Sturm
  15:00 An Expressive Model for Instance Decomposition Based Parallel SAT Solvers
    Tobias Philipp
  15:30–16:00 Coffee Break
 16:00–17:00 Session 12 (Chair: Christophe Ringeissen)
  16:00 A new Acceleration-based Combination Framework for Array Properties
    Francesco Alberti, Silvio Ghilardi, and Natasha Sharygina
  16:30 Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
    Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans

Tuesday, September 22

  09:00–10:30 Session 21 (Chair: Carsten Lutz)
  09:00 Invited Talk: Knowledge and action: how should we combine their logics?
    Andreas Herzig
  10:00 NCRL-A Model Building Approach to the Bernays-Schönfinkel Fragment
    Gábor Alagi and Christoph Weidenbach
  10:30–11:00 Coffee Break
  11:00–12:30 (Shared with TABLEAUX) Session 22 (Chair: TBA)
  11:00 Integrating Simplex with Tableaux
    David Delahaye, Guillaume Bury
  11:30 First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
    Andreas Teucke and Christoph Weidenbach
  12:00 Second-Order Quantifier Elimination on Relational Monadic Formulas — A Basic Method and Some Less Expected Applications
    Christoph Wernhardt
  12:30–14:00 Lunch
  14:00–15:30 Session 23 (Chair: TBA)
  14:00 Weakely Equivalent Arrays
    Juergen Christ and Joechen Hoenicke
  14:30 A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
    Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barret
  15:00 Adapting Real Quantifier Elimination Methods for Unsatisfiable Core Computations
    Maximilian Jaroscheck, Pablo Federico Dobal, and Pascal Fontaine
  15:30–16:00 Coffee Break
  16:00–17:30 Session 24 (Chair: TBA)
  16:00 Formalizing Soundness and Completeness of Unravelings
    Sarah Winkler and René Thiemann
  16:30 Lemmatization for Stronger Reasoning in Large Theories
    Cezary Kaliszyk, Josef Urban, and Jiri Vyskocil
  17:00 Decidable Description Logics of Context with Rigid Roles
    Stephan Böhme and Marcel Lippman

Wednesday, September 23

  09:00–10:30 (Shared with TABLEAUX) Session 31 (Chair: TBA)
  09:00 Invited Talk: TBA
    Oliver Ray
  10:00 Mīmāṃsā Deontic Logic: Proof Theory and Applications
    Agata Ciabattoni, Elisa Freschi, Björn Lellmann, Francesco Antonio Genco
  10:30–11:00 Coffee Break
 11:00–12:30 (Shared with TABLEAUX) Session 32 (Chair: TBA)
  11:00 Axiomatic constraint systems for proof search modulo theories
    Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahdoubi, and Jean-Marc Notin
  11:30 Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
    James Brotherston, Nikos Gorogiannis
  12:00 Proofs and Reconstructions
    Nik Sultana, Christoph Benzmüller, Lawrence Paulson
  12:30–14:00 Lunch
  14:00–15:30 Session 33 (Chair: TBA)
  14:00 A completion method to decide reachability in rewrite systems
    Gilles Dowek, Ying Jiang, and Guillaume Burel
  14:30 Unification and Matching in Hierarchical Combinations of Syntactic Theories
    Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, and Christophe Ringeissen
  15:00 Combining Forward and Backward Propagation
    Amira Zaki, Slim Abdennadher, and Thom Frühwirth
  15:30–16:00 Coffee Break
  16:00–17:00 TABLEAUX/FroCoS Joint Business Meeting
  18:00–23:59 Tour of Muzeum Narodowe + Banquet

Thursday, September 24

  09:00–10:30 Session 41 (Chair: TBA)
  09:00 Invited Talk: Free variables and theories: revisiting rigid E-unification
    Philipp Rümmer
  10:00 Adding Threshold Concepts to the Description Logic EL
    Franz Baader, Gerhard Brewka, and Oliver Fernandez Gil
  10:30–11:00 Coffee Break
  11:00–12:30 Session 42 (Chair: TBA)
  11:00 A Rewriting Approach to the Combination of Data Structures with Bridging Theories
    Paula Chocron, Pascal Fontaine, and Christophe Ringeissen
  11:30 Random Forests for Premise Selection
    Michael Färber and Cezary Kaliszyk
  12:00 Reasoning in Expressive Description Logics under Infinitely Valued Gödel Semantics
    Stephan Borgwardt and Rafael Peñaloza
  12:30–14:00 Lunch