ARIA

Contents:

  • Getting Started
  • Logic and Solving
  • Proofs and Explanations
  • Quantified Reasoning
    • Playing wth Quantifiers
    • Quantifier Elimination (QE)
    • Quantifier Instantiation (QI)
  • Automata and Languages
  • Verification
  • Abstraction
  • Counting, Sampling, and Probability
  • Program Synthesis
  • LLM and ML
  • CLI and Tools
  • Global Parameters
ARIA
  • Quantified Reasoning
  • View page source

Quantified Reasoning

This section focuses on quantified formulas: general background, quantifier elimination, and quantifier-instantiation-based solving.

  • Playing wth Quantifiers
    • Quantifiers
    • Solving General Quantified Problems
    • Solving Exists-Forall Problems
    • Quantifier Elimination
    • Related Work
  • Quantifier Elimination (QE)
    • Overview
    • Algorithm
    • Quantifier Elimination Tactics
    • References
  • Quantifier Instantiation (QI)
    • Overview
    • Algorithm
    • Supported Strategies
    • Supported Solvers
    • Usage
    • Configuration Options
    • Future Improvements
    • References
Previous Next

© Copyright 2024-2025, ZJU Programming Languages and Automated Reasoning Group.

Built with Sphinx using a theme provided by Read the Docs.