VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

A
Artificial Intelligence	BliStr: The Blind Strategymaker Machine Learner for Automated Reasoning 0.4 and 0.5
ATP	Beagle as a HOL4 external ATP method
ATP competitions	Machine Learner for Automated Reasoning 0.4 and 0.5
ATP process	Automated Theorem Proving using the TPTP Process Instruction Language
automated reasoning	Machine Learner for Automated Reasoning 0.4 and 0.5
automated theorem proving	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics Automated Theorem Proving using the TPTP Process Instruction Language BliStr: The Blind Strategymaker Beagle as a HOL4 external ATP method
automated theorem proving process	Automated Theorem Proving using the TPTP Process Instruction Language
B
Beagle	Beagle as a HOL4 external ATP method
C
Constraints	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
D
De Bruijn	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Description Logics	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
discrimination tree	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
E
EPR	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
equational logic	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
F
first-order logic	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
formal mathematics	Machine Learner for Automated Reasoning 0.4 and 0.5
G
geometric logic	Razor: Provenance and Exploration in Model-Finding
H
HOL4	Beagle as a HOL4 external ATP method
I
instance-based theorem proving	SGGS Theorem Proving: an Exposition
L
large theories	Machine Learner for Automated Reasoning 0.4 and 0.5
large-theory automated reasoning	BliStr: The Blind Strategymaker
Logics	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
M
machine learning	Machine Learner for Automated Reasoning 0.4 and 0.5
model finding	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
model-based theorem proving	SGGS Theorem Proving: an Exposition
model-finding	Razor: Provenance and Exploration in Model-Finding
O
OCaml	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
P
polymorphism	Polymorphic+Typeclass Superposition
prime implicates	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
prime impliquates	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
provenance	Razor: Provenance and Exploration in Model-Finding
Q
quantifier instantiation	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
S
semantic guidance	SGGS Theorem Proving: an Exposition
strategy development	BliStr: The Blind Strategymaker
substitution	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
superposition	Polymorphic+Typeclass Superposition
superposition calculus	A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
T
term representation	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
theorem proving	Polymorphic+Typeclass Superposition
TPTP	Automated Theorem Proving using the TPTP Process Instruction Language
TPTP process Instruction language	Automated Theorem Proving using the TPTP Process Instruction Language
Translation	The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics Beagle as a HOL4 external ATP method
U
Unification	Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

Disclaimer | Powered by EasyChair Smart Program