| a |
| achievements | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions |
| ACL2 | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions |
| Answer Set Programming | A Case for Query-driven Predicate Answer Set Programming |
| Applications | 24 Challenges in Deductive Software Verification |
| Artificial Intelligence | AI at CADE/IJCAR |
| automated reasoning | SC-square: when Satisfiability Checking and Symbolic Computation join forces
AI at CADE/IJCAR
The Potential of Interference-Based Proof Systems |
| automated theorem proving | We know (nearly) nothing!l But can we learn? |
| automatic theorem provers | Towards Strong Higher-Order Automation for Fast Interactive Verification |
| b |
| Big Data | Automated Reasoning for Explainable Artificial Intelligence |
| c |
| CADE | AI at CADE/IJCAR |
| calculi | The Potential of Interference-Based Proof Systems |
| certification | Beyond DRAT: Challenges in Certifying UNSAT |
| Challenges | 24 Challenges in Deductive Software Verification |
| combinations | Making Automatic Theorem Provers more Versatile |
| computer algebra | SC-square: when Satisfiability Checking and Symbolic Computation join forces |
| Conflict-driven reasoning | Automated Reasoning for Explainable Artificial Intelligence |
| d |
| deduction | We know (nearly) nothing!l But can we learn? |
| deduction modulo | Making Automatic Theorem Provers more Versatile |
| deductive software verification | 24 Challenges in Deductive Software Verification |
| DRAT | Beyond DRAT: Challenges in Certifying UNSAT |
| e |
| explanation | Automated Reasoning for Explainable Artificial Intelligence |
| f |
| first-order | Making Automatic Theorem Provers more Versatile
Do Portfolio Solvers Harm? |
| first-order logic | The Potential of Interference-Based Proof Systems
Checkable Proofs for First-Order Theorem Proving |
| formalization | Beyond DRAT: Challenges in Certifying UNSAT |
| h |
| Heuristics | We know (nearly) nothing!l But can we learn? |
| higher-order | Making Automatic Theorem Provers more Versatile |
| higher-order logic | Towards Strong Higher-Order Automation for Fast Interactive Verification |
| i |
| IJCAR | AI at CADE/IJCAR |
| industrial applications | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions |
| interactive theorem proving | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions |
| m |
| machine learning | We know (nearly) nothing!l But can we learn? |
| p |
| portfolio | Do Portfolio Solvers Harm? |
| predicate ASP | A Case for Query-driven Predicate Answer Set Programming |
| proof checking | Checkable Proofs for First-Order Theorem Proving |
| proofs | The Potential of Interference-Based Proof Systems |
| q |
| QBF | The Potential of Interference-Based Proof Systems |
| Quantifier Instantiation | Challenges for Fast Synthesis Procedures in SMT |
| s |
| SAT | Beyond DRAT: Challenges in Certifying UNSAT
Do Portfolio Solvers Harm? |
| satisfiability | The Potential of Interference-Based Proof Systems |
| satisfiability checking | SC-square: when Satisfiability Checking and Symbolic Computation join forces |
| Satisfiability Modulo Theories (SMT) | Towards Strong Higher-Order Automation for Fast Interactive Verification |
| search | We know (nearly) nothing!l But can we learn? |
| SMT | Making Automatic Theorem Provers more Versatile
Challenges for Fast Synthesis Procedures in SMT |
| solver | Do Portfolio Solvers Harm? |
| superposition calculus | Towards Strong Higher-Order Automation for Fast Interactive Verification |
| symbolic computation | SC-square: when Satisfiability Checking and Symbolic Computation join forces |
| symmetry breaking | Beyond DRAT: Challenges in Certifying UNSAT |
| synthesis | Challenges for Fast Synthesis Procedures in SMT |
| t |
| theorem prover | Do Portfolio Solvers Harm? |
| theorem proving | Checkable Proofs for First-Order Theorem Proving |
| theories | Making Automatic Theorem Provers more Versatile |
| u |
| usable automated reasoning | A Case for Query-driven Predicate Answer Set Programming |
