VSL 2014: VIENNA SUMMER OF LOGIC 2014

This page contains an index consisting of author-provided keywords.

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

Disclaimer | Powered by EasyChair Smart Program