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 |