FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

This page contains an index consisting of author-provided keywords.

A
alpha-equivalence	Reuse of Introduced Symbols in Automatic Theorem Provers
assumption-based reasoning	QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
ATP	Training ENIGMAs, CoPs, and other thinking creatures
automated reasoning	Automated Reasoning in Non-classical Logics in the TPTP World
automated theorem proving	Optimal Strategy Schedules for Everyone An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning The Logic Languages of the TPTP World and Proofs and Models in the TPTP World
Automatic program verification	Exploring Representation of Horn clauses using GNNs
Automatic theorem proving	Reuse of Introduced Symbols in Automatic Theorem Provers
B
benchmarks	The Logic Languages of the TPTP World and Proofs and Models in the TPTP World
C
CDCL	A Two-Watched Literal Scheme for First-Order Logic
clausal tableaux	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
combinators	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
condensed detachment	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
connection structure calculus	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Connection tableaux	Lazy Paramodulation in Practice
Constraint Horn clauses	Exploring Representation of Horn clauses using GNNs
COST	short COST action EuroProofNet introduction
D
decision procedure	Exploring Partial Models with SCL
Dedukti	EuroProofNet presentation on proofs in Dedukti
E
EuroProofNet	EuroProofNet presentation on SMT and proofs EuroProofNet presentation on proofs in Dedukti short COST action EuroProofNet introduction
F
first-order ATP	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
first-order logic	A Two-Watched Literal Scheme for First-Order Logic
First-order logic with equality	Lazy Paramodulation in Practice
first-order reasoning	Exploring Partial Models with SCL
First-order theorem proving	The Vampire Approach to Induction
G
grammar-based tree compression	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Graph Neural Networks	Exploring Representation of Horn clauses using GNNs
H
heuristics	Empirical Properties of Term Orderings for Superposition
Horn theories	On SGGS and Horn Clauses
I
induction	The Vampire Approach to Induction Reuse of Introduced Symbols in Automatic Theorem Provers
Isabelle	The Isabelle Community Benchmark
L
Lazy paramodulation	Lazy Paramodulation in Practice
learning	Training ENIGMAs, CoPs, and other thinking creatures
logic languages	The Logic Languages of the TPTP World and Proofs and Models in the TPTP World
M
model building	Exploring Partial Models with SCL
N
Non-classical Logic	Automated Reasoning in Non-classical Logics in the TPTP World
non-classical logics	An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
non-redundant clause learning	Exploring Partial Models with SCL
P
performance prediction	The Isabelle Community Benchmark
preprocessing	Reuse of Introduced Symbols in Automatic Theorem Provers
proof compression	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
proof schemas	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Proof search	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
proof structures	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Proofs	Training ENIGMAs, CoPs, and other thinking creatures EuroProofNet presentation on SMT and proofs EuroProofNet presentation on proofs in Dedukti short COST action EuroProofNet introduction
Python	Optimal Strategy Schedules for Everyone
Q
QBF	QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
R
run-time performance	The Isabelle Community Benchmark
S
SAT	QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Saturation	The Vampire Approach to Induction
SCL	A Two-Watched Literal Scheme for First-Order Logic
SGGS	On SGGS and Horn Clauses
shallow embedding	An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
Skolem	Reuse of Introduced Symbols in Automatic Theorem Provers
SMT	EuroProofNet presentation on SMT and proofs
strategy scheduling	Optimal Strategy Schedules for Everyone
superposition	Empirical Properties of Term Orderings for Superposition The Vampire Approach to Induction
T
term orderings	Empirical Properties of Term Orderings for Superposition
theorem proving	On SGGS and Horn Clauses The Isabelle Community Benchmark
TPTP	Lazy Paramodulation in Practice An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning The Logic Languages of the TPTP World and Proofs and Models in the TPTP World
TPTP World	Automated Reasoning in Non-classical Logics in the TPTP World
Tseitin	Reuse of Introduced Symbols in Automatic Theorem Provers
two-watched literal scheme	A Two-Watched Literal Scheme for First-Order Logic
U
user benchmark	The Isabelle Community Benchmark

Disclaimer | Powered by EasyChair Smart Program