A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets

DOI10.1016/S0747-7171(06)80009-XzbMath0796.03009OpenAlexW2010607908MaRDI QIDQ1322849

Franco Parlamento, Alberto Policriti, Eugenio Giovanni Omodeo

Publication date: 26 September 1994

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(06)80009-x

zbMATH Keywords

completenesssatisfiabilityprogram synthesiscomputable modelautomatic synthesis algorithmaxiomatic set theoriesdecision methodabstract data-typeset computationsweak theories of pure sets

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30)

Related Items

Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case ⋮ The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability

Uses Software

• ISETL

Cites Work

• A linear time solution to the single function coarsest partition problem
• Set theory in first-order logic: Clauses for Gödel's axioms
• The automation of syllogistic. I: Syllogistic normal forms
• Foundations of equational logic programming
• Towards a computation system based on set theory
• {log}: A language for programming in logic with finite sets
• Decision procedures for elementary sublanguages of set theory IX. Unsolvability of the decision problem for a restricted subclass of the Δ0-formulas in set theory
• Decision procedures for elementary sublanguages of set theory VIII. A semidecision procedure for finite satisfiability of unqualified set-theoretic formulae
• Proving termination with multiset orderings
• Expressing infinity without foundation
• A Free Variable Version of the First-Order Predicate Calculus
• Renaming a Set of Clauses as a Horn Set
• The ∀_n∃‐Completeness of Zermelo‐Fraenkel Set Theory
• Decidability of ∀*∀‐Sentences in Membership Theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item