IJCAR 2014 LNCS PROCEEDINGS: AUTHOR INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H J K L M N O P R S T W Z

A
Ansótegui, Carlos	The Fractal Dimension of SAT Formulas (PDF, talk)
Avni, Guy	From Reachability to Temporal Specifications in Cost-Sharing Games (PDF)
B
Baumgartner, Peter	Finite Quantification in Hierarchic Theorem Proving (PDF, talk)
Bax, Joshua	Finite Quantification in Hierarchic Theorem Proving (PDF, talk)
Beeson, Michael	Otter proofs in Tarskian geometry (PDF, talk)
Berdine, Josh	Computing All Implied Equalities via SMT-based Partition Refinement (PDF, talk)
Beyersdorff, Olaf	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
Biere, Armin	Unified Proof System for QBF Preprocessing (PDF, talk)
Bjorner, Nikolaj	Computing All Implied Equalities via SMT-based Partition Refinement (PDF, talk)
Blanchette, Jasmin Christian	Unified Classical Logic Completeness: A Coinductive Pearl (PDF, talk)
Bonet, Maria Luisa	The Fractal Dimension of SAT Formulas (PDF, talk)
Boudou, Joseph	Skeptik [System Description] (PDF, talk)
Bozzelli, Laura	Visibly Linear Temporal Logic (PDF, talk)
Brockschmidt, Marc	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
C
Carral, David	EL-ifying Ontologies (PDF, talk)
Cerrito, Serenella	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (PDF, talk)
Ceylan, İsmail İlkan	The Bayesian Description Logic BEL (PDF, talk)
Chew, Leroy	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
Chocron, Paula	A Gentle Non-Disjoint Combination of Satisfiability Procedures (PDF, talk)
Cortier, Veronique	Electronic voting: how logic can help (PDF)
Cuenca Grau, Bernardo	EL-ifying Ontologies (PDF, talk)
D
David, Amélie	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (PDF, talk)
Dixon, Clare	Clausal Resolution for Modal Logics of Confluence (PDF, talk)
E
Echenim, Mnacho	A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PDF, talk)
Ehlers, Rüdiger	A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (PDF, talk)
Emmes, Fabian	Proving Termination of Programs Automatically with AProVE (PDF, talk)
F
Feier, Cristina	EL-ifying Ontologies (PDF, talk)
Fellner, Andreas	Skeptik [System Description] (PDF, talk)
Fontaine, Pascal	A Gentle Non-Disjoint Combination of Satisfiability Procedures (PDF, talk)
Frohn, Florian	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
Fuhs, Carsten	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
G
Giesl, Jürgen	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
Giráldez-Cru, Jesus	The Fractal Dimension of SAT Formulas (PDF, talk)
Glimm, Birte	Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk)
Goranko, Valentin	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (PDF, talk)
Gore, Rajeev	And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (PDF, talk) A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PDF, talk) Implementing Tableaux Calculi Using BDDs: BDDTab System Description (PDF, talk)
Gorin, Daniel	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
H
Hensel, Jera	Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
Hetzl, Stefan	Introducing quantified cuts in logic with equality (PDF, talk)
Heule, Marijn	Unified Proof System for QBF Preprocessing (PDF, talk)
Hitzler, Pascal	EL-ifying Ontologies (PDF, talk)
Horbach, Matthias	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (PDF, talk)
Horrocks, Ian	EL-ifying Ontologies (PDF, talk)
J
Jeannin, Jean-Baptiste	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (PDF, talk)
K
Koopmann, Patrick	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
Kupferman, Orna	From Reachability to Temporal Specifications in Cost-Sharing Games (PDF)
L
Lahav, Ori	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk)
Lange, Martin	A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (PDF, talk)
Leitsch, Alexander	Introducing quantified cuts in logic with equality (PDF, talk)
Lellmann, Bjoern	Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (PDF, talk)
Levy, Jordi	The Fractal Dimension of SAT Formulas (PDF, talk)
Liebig, Thorsten	Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk)
Lima, Leonardo	Quati: An Automated Tool for Proving Permutation Lemmas (PDF, talk)
Lindblad, Fredrik	A Focused Sequent Calculus for Higher-Order Logic (PDF, talk)
M
Marcos, João	Clausal Resolution for Modal Logics of Confluence (PDF, talk)
McMillan, Kenneth	Structured Search and Learning (PDF, talk)
N
Nalon, Cláudia	Clausal Resolution for Modal Logics of Confluence (PDF, talk)
Nigam, Vivek	Quati: An Automated Tool for Proving Permutation Lemmas (PDF, talk)
O
Olesen, Kerry	Implementing Tableaux Calculi Using BDDs: BDDTab System Description (PDF, talk)
Olivetti, Nicola	NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (PDF, talk)
Otten, Jens	MleanCoP: A Connection Prover for First-Order Modal Logic (PDF, talk)
Otto, Carsten	Proving Termination of Programs Automatically with AProVE (PDF, talk)
P
Papacchini, Fabio	Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk)
Pattinson, Dirk	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
Pease, Adam	Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (PDF, talk)
Peltier, Nicolas	A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PDF, talk)
Peñaloza, Rafael	The Bayesian Description Logic BEL (PDF, talk)
Platzer, André	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (PDF, talk)
Plücker, Martin	Proving Termination of Programs Automatically with AProVE (PDF, talk)
Popescu, Andrei	Unified Classical Logic Completeness: A Coinductive Pearl (PDF, talk)
Pozzato, Gian Luca	NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (PDF, talk)
R
Reis, Giselle	Introducing quantified cuts in logic with equality (PDF, talk) Quati: An Automated Tool for Proving Permutation Lemmas (PDF, talk)
Ringeissen, Christophe	A Gentle Non-Disjoint Combination of Satisfiability Procedures (PDF, talk)
Ruemmer, Philipp	Approximations for Model Construction (PDF, talk)
S
Sanchez, Cesar	Visibly Linear Temporal Logic (PDF, talk)
Schmidt, Renate A.	Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk) Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
Schneider-Kamp, Peter	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
Schröder, Lutz	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
Schulz, Stephan	Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (PDF, talk)
Seidl, Martina	Unified Proof System for QBF Preprocessing (PDF, talk)
Sofronie-Stokkermans, Viorica	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (PDF, talk)
Steigmiller, Andreas	Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk)
Stroeder, Thomas	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
Stump, Aaron	StarExec: a Cross-Community Infrastructure for Logic Solving (PDF, talk)
Sutcliffe, Geoff	StarExec: a Cross-Community Infrastructure for Logic Solving (PDF, talk)
Swiderski, Steffi	Proving Termination of Programs Automatically with AProVE (PDF, talk)
T
Tamir, Tami	From Reachability to Temporal Specifications in Cost-Sharing Games (PDF)
Tapolczai, Janos	Introducing quantified cuts in logic with equality (PDF, talk)
Thiemann, Rene	Proving Termination of Programs Automatically with AProVE (PDF, talk)
Thomson, Jimmy	A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PDF, talk) Implementing Tableaux Calculi Using BDDs: BDDTab System Description (PDF, talk)
Tinelli, Cesare	StarExec: a Cross-Community Infrastructure for Logic Solving (PDF, talk)
Tourret, Sophie	A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PDF, talk)
Traytel, Dmitriy	Unified Classical Logic Completeness: A Coinductive Pearl (PDF, talk)
W
Waldmann, Uwe	Finite Quantification in Hierarchic Theorem Proving (PDF, talk)
Weller, Daniel	Introducing quantified cuts in logic with equality (PDF, talk)
Widmann, Florian	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
Wintersteiger, Christoph M.	Approximations for Model Construction (PDF, talk)
Wißmann, Thorsten	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
Woltzenlogel Paleo, Bruno	Skeptik [System Description] (PDF, talk)
Wos, Larry	Otter proofs in Tarskian geometry (PDF, talk)
Wu, Jesse	A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PDF, talk)
Z
Zeljić, Aleksandar	Approximations for Model Construction (PDF, talk)
Zhang, Wenhui	QBF Encoding of Temporal Properties and QBF-Based Verification (PDF, talk)
Zohar, Yoni	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk)