Hyperresolution and automated model building
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 549974
- Automated model building
- Automatic construction of 3-D models in multiple scale analysis
- Rule-based modelling and tunable resolution
- scientific article; zbMATH DE number 515732
- A multi-resolution workflow to generate high-resolution models constrained to dynamic data
- Multi-scale Modeling
Cited in
(33)- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Model building with ordered resolution: Extracting models from saturated clause sets
- A calculus combining resolution and enumeration for building finite models
- Hyperresolution for guarded formulae
- On the complexity of equational problems in CNF
- Positive unit hyperresolution tableaux and their application to minimal model generation
- On deciding subsumption problems
- Explicit versus implicit representations of subsets of the Herbrand universe.
- Efficient model generation through compilation.
- Working with ARMs: Complexity results on atomic representations of Herbrand models
- Blocking and other enhancements for bottom-up model generation methods
- The model evolution calculus as a first-order DPLL method
- SHR tableaux -- a framework for automated model generation
- scientific article; zbMATH DE number 515732 (Why is no real title available?)
- scientific article; zbMATH DE number 549974 (Why is no real title available?)
- Decision procedures and model building in equational clause logic
- scientific article; zbMATH DE number 1507182 (Why is no real title available?)
- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
- Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae
- scientific article; zbMATH DE number 2090304 (Why is no real title available?)
- Manipulating tree tuple languages by transforming logic programs
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- The ground-negative fragment of first-order logic is -complete
- Decidability Results for Saturation-Based Model Building
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
- Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Decision procedures using model building techniques
- A multi-resolution workflow to generate high-resolution models constrained to dynamic data
- First-order automatic literal model generation
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
- Tree tuple languages from the logic programming point of view
This page was built for publication: Hyperresolution and automated model building
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4880540)
