ARCADE 2017: Keyword Index

KeywordPapers
a
achievementsIndustrial Use of ACL2: Applications, Achievements, Challenges, and Directions
ACL2Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions
Answer Set ProgrammingA Case for Query-driven Predicate Answer Set Programming
Applications24 Challenges in Deductive Software Verification
Artificial IntelligenceAI at CADE/IJCAR
automated reasoningSC-square: when Satisfiability Checking and Symbolic Computation join forces
AI at CADE/IJCAR
The Potential of Interference-Based Proof Systems
automated theorem provingWe know (nearly) nothing!l But can we learn?
automatic theorem proversTowards Strong Higher-Order Automation for Fast Interactive Verification
b
Big DataAutomated Reasoning for Explainable Artificial Intelligence
c
CADEAI at CADE/IJCAR
calculiThe Potential of Interference-Based Proof Systems
certificationBeyond DRAT: Challenges in Certifying UNSAT
Challenges24 Challenges in Deductive Software Verification
combinationsMaking Automatic Theorem Provers more Versatile
computer algebraSC-square: when Satisfiability Checking and Symbolic Computation join forces
Conflict-driven reasoningAutomated Reasoning for Explainable Artificial Intelligence
d
deductionWe know (nearly) nothing!l But can we learn?
deduction moduloMaking Automatic Theorem Provers more Versatile
deductive software verification24 Challenges in Deductive Software Verification
DRATBeyond DRAT: Challenges in Certifying UNSAT
e
explanationAutomated Reasoning for Explainable Artificial Intelligence
f
first-orderMaking Automatic Theorem Provers more Versatile
Do Portfolio Solvers Harm?
first-order logicThe Potential of Interference-Based Proof Systems
Checkable Proofs for First-Order Theorem Proving
formalizationBeyond DRAT: Challenges in Certifying UNSAT
h
HeuristicsWe know (nearly) nothing!l But can we learn?
higher-orderMaking Automatic Theorem Provers more Versatile
higher-order logicTowards Strong Higher-Order Automation for Fast Interactive Verification
i
IJCARAI at CADE/IJCAR
industrial applicationsIndustrial Use of ACL2: Applications, Achievements, Challenges, and Directions
interactive theorem provingIndustrial Use of ACL2: Applications, Achievements, Challenges, and Directions
m
machine learningWe know (nearly) nothing!l But can we learn?
p
portfolioDo Portfolio Solvers Harm?
predicate ASPA Case for Query-driven Predicate Answer Set Programming
proof checkingCheckable Proofs for First-Order Theorem Proving
proofsThe Potential of Interference-Based Proof Systems
q
QBFThe Potential of Interference-Based Proof Systems
Quantifier InstantiationChallenges for Fast Synthesis Procedures in SMT
s
SATBeyond DRAT: Challenges in Certifying UNSAT
Do Portfolio Solvers Harm?
satisfiabilityThe Potential of Interference-Based Proof Systems
satisfiability checkingSC-square: when Satisfiability Checking and Symbolic Computation join forces
Satisfiability Modulo Theories (SMT)Towards Strong Higher-Order Automation for Fast Interactive Verification
searchWe know (nearly) nothing!l But can we learn?
SMTMaking Automatic Theorem Provers more Versatile
Challenges for Fast Synthesis Procedures in SMT
solverDo Portfolio Solvers Harm?
superposition calculusTowards Strong Higher-Order Automation for Fast Interactive Verification
symbolic computationSC-square: when Satisfiability Checking and Symbolic Computation join forces
symmetry breakingBeyond DRAT: Challenges in Certifying UNSAT
synthesisChallenges for Fast Synthesis Procedures in SMT
t
theorem proverDo Portfolio Solvers Harm?
theorem provingCheckable Proofs for First-Order Theorem Proving
theoriesMaking Automatic Theorem Provers more Versatile
u
usable automated reasoningA Case for Query-driven Predicate Answer Set Programming