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