Experiments on infinite model finding in SMT solving
From MaRDI portal
Cites work
- An automata-theoretic approach to linear temporal logic
- An introduction to mathematical logic and type theory: To truth through proof.
- Automated inference of finite unsatisfiability
- Automatic generation of logical models with AGES
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Constructing finite algebras with FALCON
- Counterexample guided inductive synthesis modulo theories
- Enumeration of AG-groupoids.
- Extending Sledgehammer with SMT solvers
- Finding finite Herbrand models
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Hammering towards QED
- HOL Light: An Overview
- scientific article; zbMATH DE number 7015112 (Why is no real title available?)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Model building with ordered resolution: Extracting models from saturated clause sets
- Predicting and detecting symmetries in FOL finite model search
- Purely Functional Data Structures
- Quantifier instantiation techniques for finite model finding in SMT
- Refutation-based synthesis in SMT
- Satisfiability modulo theories
- Scaling enumerative program synthesis via divide and conquer
- Symmetry avoidance in MACE-style finite model finding
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Towards Smarter MACE-style Model Finders
Cited in
(1)
This page was built for publication: Experiments on infinite model finding in SMT solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7025212)
