LPAR 2024C:Keyword Index

Keyword	Papers
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