| a |
| AC-completion | Ground Associative and Commutative Completion Modulo Shostak Theories |
| admissible rules | Complexity of Admissible Rules in the Implication-Negation Fragment of Intuitionistic Logic |
| Answer Set Programming | Default Reasoning in Action Domains with Conditional, Non-Local Effect Actions |
| Argumentation | Dynamics of Argumentation Systems: A Basic Theory |
| associativity and commutativity | Ground Associative and Commutative Completion Modulo Shostak Theories |
| axiom | Proof rules for the dialogical logic N |
| b |
| BCI logic | Note on Deduction Theorems in Contraction-Free Logics |
| c |
| clause elimination | Covered Clause Elimination |
| computational complexity | Complexity of Admissible Rules in the Implication-Negation Fragment of Intuitionistic Logic
Dynamics of Argumentation Systems: A Basic Theory |
| contraction-free logics | Note on Deduction Theorems in Contraction-Free Logics |
| counterexample generation | Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod |
| d |
| decision procedure | Ground Associative and Commutative Completion Modulo Shostak Theories |
| dialogical logic | Proof rules for the dialogical logic N
Playing Lorenzen Dialogue Games on the Web |
| dialogue game | Proof rules for the dialogical logic N
Playing Lorenzen Dialogue Games on the Web |
| dynamics | Dynamics of Argumentation Systems: A Basic Theory |
| f |
| feasibility | Feasibility as a gradual notion |
| g |
| gradualness | Feasibility as a gradual notion |
| Gödel logic | Gödel logics with an operator shifting truth values |
| h |
| heuristic | Playing Lorenzen Dialogue Games on the Web |
| higher-order logic | Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod |
| i |
| interactive theorem proving | Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod |
| intuitionistic logic | Complexity of Admissible Rules in the Implication-Negation Fragment of Intuitionistic Logic |
| l |
| local deduction theorems | Note on Deduction Theorems in Contraction-Free Logics |
| logical omniscience | Feasibility as a gradual notion |
| m |
| model finding | Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod |
| n |
| non-monotonic logic | Dynamics of Argumentation Systems: A Basic Theory |
| non-monotonic reasoning | Default Reasoning in Action Domains with Conditional, Non-Local Effect Actions |
| non-recursiveness | Gödel logics with an operator shifting truth values |
| o |
| object-oriented programming | Playing Lorenzen Dialogue Games on the Web |
| p |
| proof theory | Proof rules for the dialogical logic N |
| puzzle | A Sudoku-Solver for Large Puzzles using SAT |
| r |
| Reasoning about actions and change | Default Reasoning in Action Domains with Conditional, Non-Local Effect Actions |
| ring operator | Gödel logics with an operator shifting truth values |
| s |
| SAT | A Sudoku-Solver for Large Puzzles using SAT |
| SAT preprocessing | Covered Clause Elimination |
| satisfiability checking | Covered Clause Elimination |
| Shostak theories | Ground Associative and Commutative Completion Modulo Shostak Theories |
| simplification | Covered Clause Elimination |
| SMT solvers | Ground Associative and Commutative Completion Modulo Shostak Theories |
| stochastic search | A Sudoku-Solver for Large Puzzles using SAT |
| Sudoku | A Sudoku-Solver for Large Puzzles using SAT |
| t |
| t-norm logics | Feasibility as a gradual notion |
| w |
| web mathematics | Playing Lorenzen Dialogue Games on the Web |
| ł |
| Łukasiewicz logic | Gödel logics with an operator shifting truth values |
