Increasing model building capabilities by constraint solving on terms with integer exponents

DOI10.1006/JSCO.1997.0114MaRDI QIDQ1360965zbMATH OpenOpenAlexFDO

Authors Nicolas Peltier

Publication date 23 July 1997

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/bdf9263bd6dad4f118ca2d426dc775a6d65aa68c

zbMATH Keywords

\(l\)-termsdecision procedureexpressive power of constraintsmodel buildingself-resolvent clausessimultaneous search for refutations and models

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 549974
• scientific article; zbMATH DE number 1748573
• A method for building models automatically. Experiments with an extension of OTTER

Cited in

(8)

• Enhancing numerical constraint propagation using multiple inclusion representations
• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• A calculus combining resolution and enumeration for building finite models
• The first order theory of primal grammars is decidable
• A complete superposition calculus for primal grammars
• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• Perfect discrimination graphs: indexing terms with integer exponents
• Combining enumeration and deductive techniques in order to increase the class of constructible infinite models

Describes a project that uses

Uses Software

• FINDER

This page was built for publication: Increasing model building capabilities by constraint solving on terms with integer exponents

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1360965)