Talk Keyword Index

TALK KEYWORD INDEX

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

Shortcuts: A C D E F G I L P R S T V

A
automated reasoning	Alethe: Towards a Generic SMT Proof Format (Extended Abstract)
automatic theorem proving	General Automation in Coq through Modular Transformations
C
CDSAT	Proof Generation in CDSAT
certificate	A Framework for Proof-Carrying Logical Transformations
CNF	Reasoning in Many Logics with Vampire: Everything's CNF in the End
Coq	General Automation in Coq through Modular Transformations Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
COQ plugin	Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
D
deductive verification	A Framework for Proof-Carrying Logical Transformations
E
external prover	Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
F
first-order logic	General Automation in Coq through Modular Transformations
formal methods	A Framework for Proof-Carrying Logical Transformations
formal proof	Alethe: Towards a Generic SMT Proof Format (Extended Abstract)
G
Generation	Proof Generation in CDSAT
I
integer programming	Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
interactive theorem proving	General Automation in Coq through Modular Transformations
L
logical transformation	A Framework for Proof-Carrying Logical Transformations
logical transformations	General Automation in Coq through Modular Transformations
Logics	Reasoning in Many Logics with Vampire: Everything's CNF in the End
P
projective geometry	Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract)
Proof	Proof Generation in CDSAT
proof certificates	Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
proof logging	Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
pseudo-Boolean	Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
R
Reasoning	Reasoning in Many Logics with Vampire: Everything's CNF in the End
S
satisfiability	Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract)
Satisfiability Modulo Theories	Alethe: Towards a Generic SMT Proof Format (Extended Abstract)
T
theorem prover	A Framework for Proof-Carrying Logical Transformations
V
Vampire	Reasoning in Many Logics with Vampire: Everything's CNF in the End