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

DOI10.1006/JSCO.1997.0114zbMath0945.03012OpenAlexW2039470898MaRDI QIDQ1360965

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

model buildingdecision procedure\(l\)-termsexpressive power of constraintsself-resolvent clausessimultaneous search for refutations and models

Mathematics Subject Classification ID

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

Related Items (7)

The first order theory of primal grammars is decidable ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ A calculus combining resolution and enumeration for building finite models ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Perfect Discrimination Graphs: Indexing Terms with Integer Exponents ⋮ A complete superposition calculus for primal grammars

Uses Software

• FINDER

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