LPAR-20: Keyword Index

Keyword	Papers
a
Answer Set Program	Reasoning in the presence of inconsistency through Preferential ALC
automated deduction	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
b
B method	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Boolean circuits	A New Proof of P-time Completeness of Linear Lambda Calculus
c
Choose operator	Compiling Hilbert's epsilon operator
classical logic	A Lightweight Double-negation Translation
compilation	Compiling Hilbert's epsilon operator
conflict analysis	On Conflicts and Strategies in QBF
constructive logic	A Lightweight Double-negation Translation
d
deduction modulo	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Dedukti	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
Description Logic	Reasoning in the presence of inconsistency through Preferential ALC
Double negation translation	A Lightweight Double-negation Translation
e
Encoding for SMT solver	Compiling Hilbert's epsilon operator
f
first-order logic	A Lightweight Double-negation Translation
h
Hilbert's epsilon operator	Compiling Hilbert's epsilon operator
i
inconsistency-tolerant	Reasoning in the presence of inconsistency through Preferential ALC
l
linear lambda calculus	A New Proof of P-time Completeness of Linear Lambda Calculus
linear logic	A New Proof of P-time Completeness of Linear Lambda Calculus
logics	Automated Theorem Proving by Translation to Description Logic
m
MSO	Symbolic WS1S
o
opinion	Application of Trace-Based Subjective Logic to User Preferences Modeling
p
P-time Completeness	A New Proof of P-time Completeness of Linear Lambda Calculus
q
QBF	Playing with Quantified Satisfaction On Conflicts and Strategies in QBF
quantification	On Conflicts and Strategies in QBF
quantifier elimination	Playing with Quantified Satisfaction
r
Russell's definite description operator	Compiling Hilbert's epsilon operator
s
set theory	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
SMT	Playing with Quantified Satisfaction Symbolic WS1S
strategies	On Conflicts and Strategies in QBF
Subjective Logic	Application of Trace-Based Subjective Logic to User Preferences Modeling
symbolic automata	Symbolic WS1S
t
Tableau	Reasoning in the presence of inconsistency through Preferential ALC
theorem proving	Automated Theorem Proving by Translation to Description Logic
traces	Application of Trace-Based Subjective Logic to User Preferences Modeling
translation	Automated Theorem Proving by Translation to Description Logic
Typed Proof Search	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
u
user preferences	Application of Trace-Based Subjective Logic to User Preferences Modeling
v
Verification-aware programming language	Compiling Hilbert's epsilon operator
z
Zenon Modulo	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo