| 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 |
