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 |