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 |