IJCAR 2014 LNCS PROCEEDINGS: KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H I J L M N O P Q R S T U V

A
analyticity	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk)
answer set programming	Quati: An Automated Tool for Proving Permutation Lemmas (PDF, talk)
Approximations	Approximations for Model Construction (PDF, talk)
ATL+	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (PDF, talk)
Automata	Visibly Linear Temporal Logic (PDF, talk)
automated deduction	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk) Otter proofs in Tarskian geometry (PDF, talk)
automated theorem prover	MleanCoP: A Connection Prover for First-Order Modal Logic (PDF, talk)
B
background theories	Finite Quantification in Hierarchic Theorem Proving (PDF, talk)
backward proof search	A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PDF, talk)
Bayesian networks	The Bayesian Description Logic BEL (PDF, talk)
binary decision diagrams	Implementing Tableaux Calculi Using BDDs: BDDTab System Description (PDF, talk)
bounded model checking	A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (PDF, talk)
C
Circumscription	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
coalgebra	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
codatatypes	Unified Classical Logic Completeness: A Coinductive Pearl (PDF, talk)
Combination problem	A Gentle Non-Disjoint Combination of Satisfiability Procedures (PDF, talk)
Comparative evaluations	StarExec: a Cross-Community Infrastructure for Logic Solving (PDF, talk)
completeness of first-order logic	Unified Classical Logic Completeness: A Coinductive Pearl (PDF, talk)
Complex Networks	The Fractal Dimension of SAT Formulas (PDF, talk)
complexity	Proving Termination of Programs Automatically with AProVE (PDF, talk)
complexity analysis	The Bayesian Description Logic BEL (PDF, talk)
conditional logics	NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (PDF, talk)
Congruence Closure	Computing All Implied Equalities via SMT-based Partition Refinement (PDF, talk)
connection calculus	MleanCoP: A Connection Prover for First-Order Modal Logic (PDF, talk)
constrained clauses	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (PDF, talk)
constrained ordered resolution	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (PDF, talk)
context-based reasoning	The Bayesian Description Logic BEL (PDF, talk)
cut elimination	Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (PDF, talk)
cut-introduction	Introducing quantified cuts in logic with equality (PDF, talk)
Cyber-Physical Systems	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (PDF, talk)
D
data structures for tableaux calculi	Implementing Tableaux Calculi Using BDDs: BDDTab System Description (PDF, talk)
decidability	Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (PDF, talk)
decision method	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (PDF, talk)
decision procedures	Computing All Implied Equalities via SMT-based Partition Refinement (PDF, talk) QBF Encoding of Temporal Properties and QBF-Based Verification (PDF, talk) A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (PDF, talk)
Description Logics	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk) Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk) EL-ifying Ontologies (PDF, talk) The Bayesian Description Logic BEL (PDF, talk)
Differential Temporal Dynamic Logic	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (PDF, talk)
dynamic logic	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (PDF, talk)
E
equality	Introducing quantified cuts in logic with equality (PDF, talk)
equational logic	A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PDF, talk)
equational simplification	A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PDF, talk)
F
first order logic	Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (PDF, talk)
first-order logic	Finite Quantification in Hierarchic Theorem Proving (PDF, talk)
first-order modal logic	MleanCoP: A Connection Prover for First-Order Modal Logic (PDF, talk)
Fixpoints	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
Floating-Point Arithmetic	Approximations for Model Construction (PDF, talk)
focused derivations	A Focused Sequent Calculus for Higher-Order Logic (PDF, talk)
Forgetting	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
Formal Verification	Visibly Linear Temporal Logic (PDF, talk)
Fractal Dimension	The Fractal Dimension of SAT Formulas (PDF, talk)
G
geometry	Otter proofs in Tarskian geometry (PDF, talk)
global assumptions	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
global caching	A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PDF, talk) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
H
Haskell	Proving Termination of Programs Automatically with AProVE (PDF, talk)
higher-order logic	A Focused Sequent Calculus for Higher-Order Logic (PDF, talk)
Hilbert Axioms	Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (PDF, talk)
hybrid systems	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (PDF, talk)
Hypersequent Calculi	Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (PDF, talk)
I
Implementation and Optimisation Techniques	Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk)
intuitionistic	A Focused Sequent Calculus for Higher-Order Logic (PDF, talk)
intuitionistic propositional logic	A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PDF, talk)
inverse roles	Implementing Tableaux Calculi Using BDDs: BDDTab System Description (PDF, talk)
J
Java	Proving Termination of Programs Automatically with AProVE (PDF, talk)
L
lazy data structures	Unified Classical Logic Completeness: A Coinductive Pearl (PDF, talk)
local theories	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (PDF, talk)
local theory extensions	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (PDF, talk)
logic	Introducing quantified cuts in logic with equality (PDF, talk)
Logic solvers	StarExec: a Cross-Community Infrastructure for Logic Solving (PDF, talk)
lower bounds	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
M
Minimal model generation	Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk)
modal logic	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
Modal Logics	Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (PDF, talk) Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk)
Modal Logics of Confluence	Clausal Resolution for Modal Logics of Confluence (PDF, talk)
modal tableaux	Implementing Tableaux Calculi Using BDDs: BDDTab System Description (PDF, talk)
model checking	QBF Encoding of Temporal Properties and QBF-Based Verification (PDF, talk)
Model construction	Approximations for Model Construction (PDF, talk)
Model generation	Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk)
Model-checking	Visibly Linear Temporal Logic (PDF, talk)
model-finding	Finite Quantification in Hierarchic Theorem Proving (PDF, talk)
N
nested sequent calculi	NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (PDF, talk)
Nominals	COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
non-classical logics	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk)
non-deterministic semantics	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk)
Non-disjoint union of theories	A Gentle Non-Disjoint Combination of Satisfiability Procedures (PDF, talk)
non-monotonic logics	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
Number Restrictions	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
O
Ontologies	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
ontology	Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (PDF, talk)
Ontology Reasoning	Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk)
optimization	EL-ifying Ontologies (PDF, talk)
Otter	Otter proofs in Tarskian geometry (PDF, talk)
OWL 2 EL	EL-ifying Ontologies (PDF, talk)
P
Permutation lemmas	Quati: An Automated Tool for Proving Permutation Lemmas (PDF, talk)
pointer arithmetic	Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
preprocessing	Unified Proof System for QBF Preprocessing (PDF, talk)
primal infon logic	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk)
prime implicates	A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PDF, talk)
program analysis	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
Prolog	Proving Termination of Programs Automatically with AProVE (PDF, talk)
proof checking	Unified Proof System for QBF Preprocessing (PDF, talk)
proof complexity	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
proof compression	Introducing quantified cuts in logic with equality (PDF, talk) Skeptik [System Description] (PDF, talk)
proof search	A Focused Sequent Calculus for Higher-Order Logic (PDF, talk)
proof theory	Quati: An Automated Tool for Proving Permutation Lemmas (PDF, talk)
propositional logics	QBF Encoding of Temporal Properties and QBF-Based Verification (PDF, talk)
Propositional Normal Modal logics	Clausal Resolution for Modal Logics of Confluence (PDF, talk)
Propositional Resolution	Skeptik [System Description] (PDF, talk)
Q
QBF	Unified Proof System for QBF Preprocessing (PDF, talk)
R
reduction to SAT	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk)
resolution	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
resolution method	Clausal Resolution for Modal Logics of Confluence (PDF, talk)
Rewriting	EL-ifying Ontologies (PDF, talk)
S
SAT	The Fractal Dimension of SAT Formulas (PDF, talk)
SAT Features	The Fractal Dimension of SAT Formulas (PDF, talk)
SAT solver	A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (PDF, talk)
satisfiability	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (PDF, talk) Skeptik [System Description] (PDF, talk)
Satisfiability Modulo Theories	Computing All Implied Equalities via SMT-based Partition Refinement (PDF, talk) Skeptik [System Description] (PDF, talk)
Satisfiability procedure	A Gentle Non-Disjoint Combination of Satisfiability Procedures (PDF, talk)
saturation	Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (PDF, talk)
Saturation Procedures	Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk)
Scala	Skeptik [System Description] (PDF, talk)
Self-similarity	The Fractal Dimension of SAT Formulas (PDF, talk)
sequent Calculi	SAT-based Decision Procedure for Analytic Pure Sequent Calculi (PDF, talk) A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PDF, talk) The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
sequent calculus	A Focused Sequent Calculus for Higher-Order Logic (PDF, talk)
SHOIQ	EL-ifying Ontologies (PDF, talk)
SHQ	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
simulations	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
SMT	Approximations for Model Construction (PDF, talk)
SMT-solving	Finite Quantification in Hierarchic Theorem Proving (PDF, talk)
Software Verification	Computing All Implied Equalities via SMT-based Partition Refinement (PDF, talk)
Solver competitions	StarExec: a Cross-Community Infrastructure for Logic Solving (PDF, talk)
Solver execution services	StarExec: a Cross-Community Infrastructure for Logic Solving (PDF, talk)
string processing	Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
strong termination	Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk)
Subset-simulation	Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk)
System description	Quati: An Automated Tool for Proving Permutation Lemmas (PDF, talk)
T
Tableau	The Complexity of Theorem Proving in Circumscription and Minimal Entailment (PDF, talk)
Tableau Algorithms	Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures (PDF, talk)
tableaux	Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (PDF, talk) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (PDF, talk)
tableaux calculus	Terminating Minimal Model Generation Procedures for Propositional Modal Logics (PDF, talk)
Tarski	Otter proofs in Tarskian geometry (PDF, talk)
temporal logic	dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (PDF, talk) A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (PDF, talk) Visibly Linear Temporal Logic (PDF, talk)
temporal logics	QBF Encoding of Temporal Properties and QBF-Based Verification (PDF, talk)
term rewriting	Proving Termination of Programs Automatically with AProVE (PDF, talk)
termination	Proving Termination of Programs Automatically with AProVE (PDF, talk) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (PDF, talk)
theorem proving	Unified Classical Logic Completeness: A Coinductive Pearl (PDF, talk) NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (PDF, talk) Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (PDF, talk)
Theorem-Proving	Clausal Resolution for Modal Logics of Confluence (PDF, talk)
tool support	A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (PDF, talk)
U
uncertainty reasoning	The Bayesian Description Logic BEL (PDF, talk)
Uniform Interpolation	Count and Forget: Uniform Interpolation of SHQ-Ontologies (PDF, talk)
V
verification	QBF Encoding of Temporal Properties and QBF-Based Verification (PDF, talk)
Visibly Pushdown Languages	Visibly Linear Temporal Logic (PDF, talk)