LPAR 2024C: Keyword Index

KeywordPapers
a
admissibilityA System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
Andrews-Curtis conjectureTowards computer-assisted proofs of parametric Andrews-Curtis simplifications, II
arraysOn SMT Theory Design: The Case of Sequences
automated reasoningAutomated Reasoning with Tangles: towards Quantum Verification Applications
Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II
automated theorem provingAutomated Theorem Proving for Prolog Verification
b
base conversionNumeric Base Conversion with Rewriting
Bubble SortCertification of Tail Recursive Bubble--Sort in Theorema and Coq
c
certificationCertification of Tail Recursive Bubble--Sort in Theorema and Coq
combinatorial group theoryTowards computer-assisted proofs of parametric Andrews-Curtis simplifications, II
CoqCertification of Tail Recursive Bubble--Sort in Theorema and Coq
d
Description LogicsA Case for Extensional Non-Wellfounded Metamodeling
f
FusionOn Symbolic Derivatives and Transition Regexes
g
guarded commandsAlternate Semantics of the Guarded Conditional
i
Inductive proofsOn Proof Schemata and Primitive Recursive Arithmetic
InferentialismA System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
intuitionistic logicA System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
involutory quandlesAutomated Reasoning with Tangles: towards Quantum Verification Applications
k
knowledge representationA Case for Extensional Non-Wellfounded Metamodeling
l
logicOn SMT Theory Design: The Case of Sequences
A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
logic programmingAutomated Theorem Proving for Prolog Verification
lookaheadOn Symbolic Derivatives and Transition Regexes
m
MetamodelingA Case for Extensional Non-Wellfounded Metamodeling
n
Natural-style ProvingA Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation
nondeterminismAlternate Semantics of the Guarded Conditional
numeric basesNumeric Base Conversion with Rewriting
o
OntologiesA Case for Extensional Non-Wellfounded Metamodeling
operational semanticsAlternate Semantics of the Guarded Conditional
p
partial correctnessAutomated Theorem Proving for Prolog Verification
primitive recursive arithmeticOn Proof Schemata and Primitive Recursive Arithmetic
PrologAutomated Theorem Proving for Prolog Verification
Proof SchemaOn Proof Schemata and Primitive Recursive Arithmetic
proof theoryA System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
proof-theoretic semanticsA System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic
propositional logicA Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation
q
quantum verificationAutomated Reasoning with Tangles: towards Quantum Verification Applications
s
Satisfiability Modulo TheoriesOn SMT Theory Design: The Case of Sequences
sequencesOn SMT Theory Design: The Case of Sequences
sequent calculusA Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation
set theoryA Case for Extensional Non-Wellfounded Metamodeling
SMTOn Symbolic Derivatives and Transition Regexes
sortingCertification of Tail Recursive Bubble--Sort in Theorema and Coq
symbolic automatonOn Symbolic Derivatives and Transition Regexes
t
tanglesAutomated Reasoning with Tangles: towards Quantum Verification Applications
temporal logicOn Symbolic Derivatives and Transition Regexes
term rewritingNumeric Base Conversion with Rewriting
terminationAutomated Theorem Proving for Prolog Verification
TheoremaCertification of Tail Recursive Bubble--Sort in Theorema and Coq
A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation
u
Unit PropagationA Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation
v
verificationAutomated Theorem Proving for Prolog Verification