Printable version available here





































Workshops
Session 1

Tableaux S1
FroCoS S1, joint with Tableaux
Joint FroCoS + Tableaux
FroCoS starts at 9:30


Tobias Nipkow
Lawrence C. Paulson
Stéphane Demri
FroCoS S7


+1 regular paper
+1 regular paper
+1 regular paper
Konstantin Korovin

Coffee
Coffee
Coffee
Coffee
Coffee

Workshops
Session 2

Tableaux S2
Tableaux FroCoS S2
Tableaux S7 FroCoS S4
FroCoS S8


 
Tutorials  
   
 


 
until 13:00  
   
 





 

FroCoS Business Meeting


Lunch
Lunch
Lunch
Lunch
Lunch













Workshops
Session 3

Tableaux S3
Tableaux S5, joint with FroCoS
FroCoS S5, joint with Tableaux
FroCoS S9


 
Sara Negri
Joël Ouaknine
 


 
+1 regular paper
+1 regular paper
 

Coffee
Coffee
Coffee
Coffee
Coffee

Workshops
Session 4

Tableaux S4
Tableaux S6 FroCoS S3
Tableaux S8 FroCoS S6



until 17:00
   
   





   
   






Tableaux Business Meeting






















Tableaux reception
FroCoS reception
FroCoS + Tableaux Dinner






starting 18:15
starting 19:00
starting 19:30


Color code:FroCoS event
Tableaux event
FroCoS + Tableaux event


Wednesday, 18 September 2013

08:30 - 08:55 Registration
08:55 - 09:00 Welcome
FroCoS Session 1 Chair: Pascal Fontaine
09:00 - 10:00 Keynote speaker: Lawrence C. Paulson
MetiTarski's Menagerie of Cooperating Systems
10:00 - 10:30 Abdelkader Kersani and Nicolas Peltier
Combining Superposition and Induction: A Practical Realization
10:30 - 11:00 Coffee break
FroCoS Session 2 Chair: Christophe Ringeissen
11:00 - 11:30 Francesco Alberti, Silvio Ghilardi and Natasha Sharygina
Definability of Accelerated Relations in a Theory of Arrays and Its Applications
11:30 - 12:00 Clara Bertolissi and Silvio Ranise
Verification of Composed Array-based Systems with Applications to Security-Aware Workflows
12:00 - 12:30 Ralf Karrenberg, Marek Košta and Thomas Sturm
Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
12:30 - 14:00 Lunch break
Tableaux Session 5 Chair: Dale Miller
14:00 - 15:00 Keynote speaker: Sara Negri
On the Duality of Proofs and Countermodels in Labelled Sequent Calculi
15:00 - 15:30
Tableaux paper
Zhé Hóu, Alwen Tiu and Rajeev Goré
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
15:30 - 16:00 Coffee break
FroCoS Session 3 Chair: Roberto Sebastiani
16:00 - 16:30 Rafael Peñaloza and Tingting Zou
Roughening the EL Envelope
16:30 - 17:00 Patrick Koopmann and Renate A. Schmidt
Uniform Interpolation of ALC-Ontologies Using Fixpoints
17:00 - 17:30 Christoph Wernhard
Abduction in Logic Programming as Second-Order Quantifier Elimination
Social Program
19:00 - FroCoS reception
Musée Lorrain (64, Grande Rue, 54000 Nancy)
Short visit followed by reception


Thursday, 19 September 2013

Joint Session Chair: Silvio Ghilardi
09:00 - 10:00 Keynote speaker: Stéphane Demri
Witness Runs for Counter Machines
Joint work with Clark Barrett and Morgan Deters
10:00 - 10:30
Tableaux paper
Joseph Boudou and Bruno Woltzenlogel Paleo
Compression of Propositional Resolution Proofs by Lowering Subproofs
10:30 - 11:00 Coffee break
FroCoS Session 4 Chair: Renate Schmidt
11:00 - 11:30 Philippe Balbiani and Szabolcs Mikulás
Decidability and Complexity via Mosaics of the Temporal Logic of the Lexicographic Products of Unbounded Dense Linear Orders
11:30 - 12:00 Stefan Borgwardt, Marcel Lippmann and Veronika Thost
Temporal Query Answering in the Description Logic DL-Lite
12:00 - 12:30 Franz Baader and Benjamin Zarrieß
Verification of Golog Programs over Description Logic Actions
12:30 - 13:00 FroCoS Business Meeting
12:30 - 14:00 Lunch break
FroCoS Session 5 Chair: Silvio Ranise
14:00 - 15:00 Keynote speaker: Joël Ouaknine
Specification and Verification of Linear Dynamical Systems: Advances and Challenges
15:00 - 15:30 Matthias Horbach and Viorica Sofronie-Stokkermans
Obtaining Finite Local Theory Axiomatizations via Saturation
15:30 - 16:00 Coffee break
FroCoS Session 6 Chair: Christoph Weidenbach
16:00 - 16:30 Konstantin Korovin
Non-Cyclic Sorts for First-Order Satisfiability
16:30 - 17:00 Guillaume Burel and Simon Cruanes
Detection of First Order Axiomatic Theories
17:00 - 17:30 Jasmin Christian Blanchette and Andrei Popescu
Mechanizing the Metatheory of Sledgehammer
Social Program
19:30 - Conference dinner
Grand Hôtel de la Reine (2, Place Stanislas, 54000 Nancy)


Friday, 20 September 2013

FroCoS Session 7 Chair: Peter Baumgartner
09:30 - 10:30 Keynote speaker: Konstantin Korovin
From Resolution and DPLL to Solving Arithmetic Constraints
10:30 - 11:00 Coffee break
FroCoS Session 8 Chair: Didier Galmiche
11:00 - 11:30 Carlos Areces, Raul Fervari and Guillaume Hoffmann
Tableaux for Relation-Changing Modal Logics
11:30 - 12:00 Fabio Papacchini and Renate A. Schmidt
Computing Minimal Models Modulo Subset-Simulation for Modal Logics
12:00 - 12:30 Franz Baader, Oliver Fernández Gil and Barbara Morawska
Hybrid Unification in the Description Logic EL
12:30 - 14:00 Lunch break
FroCoS Session 9 Chair: Franz Baader
14:00 - 14:30 Takahito Aoto
Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering
14:30 - 15:00 Christopher Bouchard, Kimberly A. Gero, Christopher Lynch and Paliath Narendran
On Forward Closure and the Finite Variant Property
15:00 - 15:30 Cynthia Kop and Naoki Nishida
Term Rewriting with Logical Constraints
15:30 - 16:00 Coffee break