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 |