


default search action
9. FroCos 2013: Nancy, France
- Pascal Fontaine, Christophe Ringeissen, Renate A. Schmidt:
Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings. Lecture Notes in Computer Science 8152, Springer 2013, ISBN 978-3-642-40884-7
Invited Talk 1
- Lawrence C. Paulson
:
MetiTarski's Menagerie of Cooperating Systems. 1-6
Inductive Theorem Proving
- Abdelkader Kersani, Nicolas Peltier:
Combining Superposition and Induction: A Practical Realization. 7-22
Arrays and Memory Access Optimization
- Francesco Alberti, Silvio Ghilardi
, Natasha Sharygina:
Definability of Accelerated Relations in a Theory of Arrays and Its Applications. 23-39 - Clara Bertolissi, Silvio Ranise
:
Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows. 40-55 - Ralf Karrenberg, Marek Kosta, Thomas Sturm
:
Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages. 56-70
Approximation and Forgetting
- Rafael Peñaloza
, Tingting Zou:
Roughening the Envelope. 71-86 - Patrick Koopmann
, Renate A. Schmidt
:
Uniform Interpolation of -Ontologies Using Fixpoints. 87-102 - Christoph Wernhard:
Abduction in Logic Programming as Second-Order Quantifier Elimination. 103-119
Invited Talk 2
- Clark W. Barrett
, Stéphane Demri, Morgan Deters:
Witness Runs for Counter Machines. 120-150
Temporal and Description Logic Techniques
- Philippe Balbiani
, Szabolcs Mikulás:
Decidability and Complexity via Mosaics of the Temporal Logic of the Lexicographic Products of Unbounded Dense Linear Orders. 151-164 - Stefan Borgwardt
, Marcel Lippmann, Veronika Thost:
Temporal Query Answering in the Description Logic DL-Lite. 165-180 - Franz Baader
, Benjamin Zarrieß:
Verification of Golog Programs over Description Logic Actions. 181-196
Invited Talk 3
- Joël Ouaknine:
Specification and Verification of Linear Dynamical Systems: Advances and Challenges. 197
Theorem Proving with Theories and Sorts
- Matthias Horbach, Viorica Sofronie-Stokkermans:
Obtaining Finite Local Theory Axiomatizations via Saturation. 198-213 - Konstantin Korovin:
Non-cyclic Sorts for First-Order Satisfiability. 214-228 - Guillaume Burel, Simon Cruanes
:
Detection of First Order Axiomatic Theories. 229-244 - Jasmin Christian Blanchette, Andrei Popescu:
Mechanizing the Metatheory of Sledgehammer. 245-260
Invited Talk 4
- Konstantin Korovin:
From Resolution and DPLL to Solving Arithmetic Constraints. 261-262
Modal Logic and Description Logic
- Carlos Areces
, Raul Fervari
, Guillaume Hoffmann:
Tableaux for Relation-Changing Modal Logics. 263-278 - Fabio Papacchini, Renate A. Schmidt
:
Computing Minimal Models Modulo Subset-Simulation for Modal Logics. 279-294 - Franz Baader
, Oliver Fernandez Gil
, Barbara Morawska
:
Hybrid Unification in the Description Logic. 295-310
Rewriting
- Takahito Aoto:
Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering. 311-326 - Christopher Bouchard, Kimberly A. Gero, Christopher Lynch, Paliath Narendran:
On Forward Closure and the Finite Variant Property. 327-342 - Cynthia Kop, Naoki Nishida:
Term Rewriting with Logical Constraints. 343-358

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.