a |

admissibility | A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic |

Andrews-Curtis conjecture | Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II |

arrays | On SMT Theory Design: The Case of Sequences |

automated reasoning | Automated Reasoning with Tangles: towards Quantum Verification Applications Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II |

automated theorem proving | Automated Theorem Proving for Prolog Verification |

b |

base conversion | Numeric Base Conversion with Rewriting |

Bubble Sort | Certification of Tail Recursive Bubble--Sort in Theorema and Coq |

c |

certification | Certification of Tail Recursive Bubble--Sort in Theorema and Coq |

combinatorial group theory | Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II |

Coq | Certification of Tail Recursive Bubble--Sort in Theorema and Coq |

d |

Description Logics | A Case for Extensional Non-Wellfounded Metamodeling |

f |

Fusion | On Symbolic Derivatives and Transition Regexes |

g |

guarded commands | Alternate Semantics of the Guarded Conditional |

i |

Inductive proofs | On Proof Schemata and Primitive Recursive Arithmetic |

Inferentialism | A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic |

intuitionistic logic | A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic |

involutory quandles | Automated Reasoning with Tangles: towards Quantum Verification Applications |

k |

knowledge representation | A Case for Extensional Non-Wellfounded Metamodeling |

l |

logic | On SMT Theory Design: The Case of Sequences A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic |

logic programming | Automated Theorem Proving for Prolog Verification |

lookahead | On Symbolic Derivatives and Transition Regexes |

m |

Metamodeling | A Case for Extensional Non-Wellfounded Metamodeling |

n |

Natural-style Proving | A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation |

nondeterminism | Alternate Semantics of the Guarded Conditional |

numeric bases | Numeric Base Conversion with Rewriting |

o |

Ontologies | A Case for Extensional Non-Wellfounded Metamodeling |

operational semantics | Alternate Semantics of the Guarded Conditional |

p |

partial correctness | Automated Theorem Proving for Prolog Verification |

primitive recursive arithmetic | On Proof Schemata and Primitive Recursive Arithmetic |

Prolog | Automated Theorem Proving for Prolog Verification |

Proof Schema | On Proof Schemata and Primitive Recursive Arithmetic |

proof theory | A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic |

proof-theoretic semantics | A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic |

propositional logic | A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation |

q |

quantum verification | Automated Reasoning with Tangles: towards Quantum Verification Applications |

s |

Satisfiability Modulo Theories | On SMT Theory Design: The Case of Sequences |

sequences | On SMT Theory Design: The Case of Sequences |

sequent calculus | A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation |

set theory | A Case for Extensional Non-Wellfounded Metamodeling |

SMT | On Symbolic Derivatives and Transition Regexes |

sorting | Certification of Tail Recursive Bubble--Sort in Theorema and Coq |

symbolic automaton | On Symbolic Derivatives and Transition Regexes |

t |

tangles | Automated Reasoning with Tangles: towards Quantum Verification Applications |

temporal logic | On Symbolic Derivatives and Transition Regexes |

term rewriting | Numeric Base Conversion with Rewriting |

termination | Automated Theorem Proving for Prolog Verification |

Theorema | Certification of Tail Recursive Bubble--Sort in Theorema and Coq A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation |

u |

Unit Propagation | A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation |

v |

verification | Automated Theorem Proving for Prolog Verification |