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 |