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 |