IJCAR Program

10:45	Rajeev Gore And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (abstract)
11:45	Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel Unified Classical Logic Completeness: A Coinductive Pearl (abstract)
12:15	Fredrik Lindblad A Focused Sequent Calculus for Higher-Order Logic (abstract)

13:00-14:30Lunch Break

14:30-16:00 Session 113C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with CAV)

Chair:

Roberto Sebastiani

Location: FH, Hörsaal 5

14:30	Ori Lahav and Yoni Zohar SAT-based Decision Procedure for Analytic Pure Sequent Calculi (abstract)
15:00	Marijn Heule, Martina Seidl and Armin Biere A Unified Proof System for QBF Preprocessing (abstract)
15:30	Carlos Ansótegui, Maria Luisa Bonet, Jesus Giráldez-Cru and Jordi Levy The Fractal Dimension of SAT Formulas (abstract)

16:00-16:30Coffee Break

16:30-17:00 Session 116C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with CAV)

Chair:

Uwe Waldmann

Location: FH, Hörsaal 5

16:30

Paula Chocron, Pascal Fontaine and Christophe Ringeissen

A Gentle Non-Disjoint Combination of Satisfiability Procedures (abstract)

17:00-17:10 Session 118: Best Paper Award Ceremony

Chair:

Christoph Weidenbach

Location: FH, Hörsaal 5

17:10-18:00 Session 119B: Herbrand Award Ceremony

Chair:

Maria Paola Bonacina

Location: FH, Hörsaal 5

19:00-21:30 Session 122: VSL Reception 2

Location: University of Vienna, Arkadenhof

Sunday, July 20th, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

08:45-10:15 Session 123: FLoC Plenary Talk (joint with 9 other meetings)

Chair:

Andrei Voronkov

Location: FH, Hörsaal 1

08:45

Véronique Cortier

FLoC Plenary Talk: Electronic voting: how logic can help? (abstract)

Saturday, July 19th, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

22:00-23:59 Session 123: VSL Student Reception 2

Location: Säulenhalle (Volksgarten)

Sunday, July 20th, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

10:15-10:45Coffee Break

10:15-18:00 Session 126A: FLoC Olympic Games Big Screen: CASC Automated Theorem Proving System Competition (CASC-J7) (joint with 9 other meetings)

Location: FH, 2nd floor

10:15

Geoff Sutcliffe

FLoC Olympic Games Big Screen: 7th IJCAR ATP System Competition (CASC-J7) (abstract)

10:15-18:00 Session 126B: FLoC Olympic Games Big Screen: Termination Competition (termComp) (joint with 9 other meetings)

Location: FH, 2nd floor

10:15

Jürgen Giesl, Stefan von der Krone, Frederic Mesnard, Albert Rubio, René Thiemann and Johannes Waldmann

FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014) (abstract)

10:45-13:00 Session 127E: Equational Reasoning

Chair:

Deepak Kapur

Location: FH, Hörsaal 5

10:45	Sophie Tourret, Mnacho Echenim and Nicolas Peltier A Rewriting Strategy to Generate Prime Implicates in Equational Logic (abstract)
11:15	Peter Baumgartner, Joshua Bax and Uwe Waldmann Finite Quantification in Hierarchic Theorem Proving (abstract)
11:45	Josh Berdine and Nikolaj Bjorner Computing All Implied Equalities via SMT-based Partition Refinement (abstract)
12:15	Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Stroeder, Steffi Swiderski and Rene Thiemann Proving Termination of Programs Automatically with AProVE (abstract)

13:00-14:30Lunch Break

14:30-16:00 Session 129E: Verification

Chair:

Aart Middeldorp

Location: FH, Hörsaal 5

14:30	Matthias Horbach and Viorica Sofronie-Stokkermans Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (abstract)
15:00	Thomas Stroeder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel and Peter Schneider-Kamp Proving Termination and Memory Safety for Programs with Pointer Arithmetic (abstract)
15:30	Wenhui Zhang QBF Encoding of Temporal Properties and QBF-Based Verification (abstract)

14:30-16:00 Session 129G: FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (joint with 9 other meetings)

Location: FH, Hörsaal 2

14:30

Francesco Calimeri, Martin Gebser, Marco Maratea and Francesco Ricca

FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (abstract)

16:00-16:30Coffee Break

16:30-18:00 Session 130E: Proof Theory

Chair:

Jürgen Giesl

Location: FH, Hörsaal 5

16:30	Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai and Daniel Weller Introducing quantified cuts in logic with equality (abstract)
17:00	Vivek Nigam, Giselle Reis and Leonardo Lima Quati: An Automated Tool for Proving Permutation Lemmas (abstract)
17:20	Rajeev Gore, Jimmy Thomson and Jesse Wu A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (abstract)
17:40	Jens Otten MleanCoP: A Connection Prover for First-Order Modal Logic (abstract)

Monday, July 21st, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

10:45-13:05 Session 138E: Modal and Temporal Reasoning

Chair:

Renate Schmidt

Location: FH, Hörsaal 5

10:45	Serenella Cerrito, Amélie David and Valentin Goranko Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (abstract)
11:15	Jean-Baptiste Jeannin and André Platzer dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (abstract)
11:45	Bjoern Lellmann Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (abstract)
12:15	Cláudia Nalon, João Marcos and Clare Dixon Clausal Resolution for Modal Logics of Confluence (abstract)
12:45	Rajeev Gore, Jimmy Thomson and Kerry Olesen Implementing Tableaux Calculi Using BDDs: BDDTab System Description (abstract)

14:30-16:00 Session 140E: FLoC Inter-Conference topic: SAT/SMT/QBF (joint with CAV)

Chair:

Pascal Fontaine

Location: FH, Hörsaal 5

14:30	Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Ruemmer Approximations for Model Construction (abstract)
15:00	Rüdiger Ehlers and Martin Lange A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (abstract)
15:20	Aaron Stump, Geoff Sutcliffe and Cesare Tinelli StarExec: a Cross-Community Infrastructure for Logic Solving (abstract)
15:40	Bruno Woltzenlogel Paleo, Joseph Boudou and Andreas Fellner Skeptik [System Description] (abstract)

16:00-16:50 Session 142: Modal Logic

Chair:

Silvio Ghilardi

Location: FH, Hörsaal 5

16:00	Fabio Papacchini and Renate A. Schmidt Terminating Minimal Model Generation Procedures for Propositional Modal Logics (abstract)
16:30	Daniel Gorin, Dirk Pattinson, Lutz Schröder, Thorsten Wißmann and Florian Widmann COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (abstract)

Sunday, July 20th, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

19:00-21:30 Session 142: VSL Banquet 2

Location: Schönbrunn

Monday, July 21st, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

16:50-17:20 Session 144: In memoriam: Bernhard Gramlich

Chair:

Maria Paola Bonacina

Location: FH, Hörsaal 5

08:45-10:15 Session 144A: VSL Keynote Talk

Chair:

Thomas Eiter

Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1

08:45

Franz Baader

VSL Keynote Talk: Ontology-Based Monitoring of Dynamic Systems (abstract)

10:15-10:45Coffee Break

13:00-14:30Lunch Break

16:00-16:30Coffee Break

17:20-18:00 Session 145: CADE / FROCOS / TABLEAUX / IJCAR Business Meetings

Chair:

Maria Paola Bonacina

Location: FH, Hörsaal 5

19:00-20:00 Session 149A: VSL Public Lecture 2

Location: MB, Kuppelsaal

19:00

Friedrich Stadler

VSL Public Lecture: Vienna Circle(s) - Between Philosophy and Science in Cultural Context (abstract)

Tuesday, July 22nd, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

10:45-13:05 Session 149C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with CAV)

Chair:

Orna Grumberg

Location: FH, Hörsaal 1

10:45	Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg Monadic Decomposition (abstract)
11:05	Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Morgan Deters A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (abstract)
11:25	Alexander Nadel Bit-Vector Rewriting with Automatic Rule Generation (abstract)
11:45	Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli and Kshitij Bansal A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (abstract)
12:05	Andrei Voronkov AVATAR: The New Architecture for First-Order Theorem Provers (abstract)
12:25	Ruzica Piskac, Thomas Wies and Damien Zufferey Automating Separation Logic with Trees and Data (abstract)
12:45	Ashish Tiwari and Patrick Lincoln A Nonlinear Real Arithmetic Fragment (abstract)
12:55	Bruno Dutertre Yices 2.2 (abstract)

10:45-13:00 Session 149E: Invited talk & Complexity

Chair:

Christoph Weidenbach

Location: FH, Hörsaal 5

10:45	Kenneth McMillan Structured Search and Learning (abstract)
11:45	Olaf Beyersdorff and Leroy Chew The Complexity of Theorem Proving in Circumscription and Minimal Entailment (abstract)
12:15	Laura Bozzelli and Cesar Sanchez Visibly Linear Temporal Logic (abstract)

Monday, July 21st, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

16:30-19:00 Session 151A: VSL Joint Award Ceremony 2

Chair:

Helmut Veith

Location: MB, Kuppelsaal

16:30	Floc Olympic Games FLoC Olympic Games Award Ceremony 2 (abstract)
18:00	Werner Depauli-Schimanovich Lifetime Achievement Award (abstract)
18:10	Mingyi Zhang Lifetime Achievement Award (abstract)
18:20	European Masters Program In Computational Logic EMCL Distinguished Alumni Award (abstract)
18:30	Helmut Veith FLoC Closing Week 2 (abstract)

Tuesday, July 22nd, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

14:30-16:00 Session 151E: Description Logic

Chair:

Peter Baumgartner

Location: FH, Hörsaal 5

14:30	Patrick Koopmann and Renate A. Schmidt Count and Forget: Uniform Interpolation of SHQ-Ontologies (abstract)
15:00	Andreas Steigmiller, Birte Glimm and Thorsten Liebig Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures (abstract)
15:30	David Carral, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler and Ian Horrocks EL-ifying Ontologies (abstract)

16:30-18:10 Session 153B: Knowledge Representation & Reasoning

Chair:

Geoff Sutcliffe

Location: FH, Hörsaal 5

16:30	İsmail İlkan Ceylan and Rafael Peñaloza The Bayesian Description Logic BEL (abstract)
17:00	Michael Beeson and Larry Wos Otter proofs of theorems in Tarskian geometry (abstract)
17:30	Nicola Olivetti and Gian Luca Pozzato NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (abstract)
17:50	Adam Pease and Stephan Schulz Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (abstract)

08:45-10:15 Session 156: VSL Keynote Talk

Chair:

Helmut Veith

Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1

08:45

Edmund Clarke

VSL Keynote Talk: Verification of Computer Systems with Model Checking (abstract)

10:15-10:45Coffee Break

13:00-14:30Lunch Break

16:00-16:30Coffee Break