scientific article

Publication date: 1979

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

quantificational formulas solvable classes Herbrand expansions

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25)

Related Items

Some results on the containment and minimization of (in)equality queries ⋮ Three-variable statements of set-pairing ⋮ Combining Theories: The Ackerman and Guarded Fragments ⋮ Asymptotic probabilities of existential second-order Gödel sentences ⋮ Undecidability of modal and intermediate first-order logics with two individual variables ⋮ Random models and solvable Skolem classes ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ The ∀∃-theory of ℛ(≤,∨,∧) is undecidable ⋮ Decidability and completeness for open formulas of membership theories ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Using resolution for deciding solvable classes and building finite models ⋮ Implication of clauses is undecidable ⋮ Random models and the Maslov class ⋮ Structured proof procedures ⋮ Decidability of ∀*∀‐Sentences in Membership Theories ⋮ Complexity results for classes of quantificational formulas ⋮ On the Decision Problem for Two-Variable First-Order Logic ⋮ Automatic theorem proving. II ⋮ The Mathematical Development of Set Theory from Cantor to Cohen ⋮ Asymptotic conditional probabilities: The non-unary case ⋮ 0-1 laws and decision problems for fragments of second-order logic ⋮ Techniques of computable set theory with applications to proof verification ⋮ Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case ⋮ Description of restricted automata by first-order formulae ⋮ A decision procedure revisited: Notes on direct logic, linear logic and its implementation ⋮ The Gödel class with identity is unsolvable ⋮ Random models and the Gödel case of the decision problem ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ A theory of abstraction ⋮ The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability ⋮ Finite-model theory -- A personal perspective ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Program schemata and the first-order decision problem ⋮ From Philosophical to Industrial Logics ⋮ Maslov's inverse method and decidable classes ⋮ Quine's ‘limits of decision’ ⋮ Counterexamples of the 0-1 Law for Fragments of Existential Second-Order Logic: an Overview ⋮ An analysis of first-order logics of probability ⋮ Combinations of Theories for Decidable Fragments of First-Order Logic ⋮ Deciding the \(E^+\)-class by an a posteriori, liftable order ⋮ Turning decision procedures into disprovers ⋮ Deciding simple infinity axiom sets with one binary relation by means of superpostulates ⋮ Automated theorem proving methods ⋮ Tractable reasoning via approximation ⋮ The complexity of the satisfiability problem for Krom formulas ⋮ Conservative reduction classes of Krom formulas ⋮ Thue trees ⋮ Inclusion dependencies and their interaction with functional dependencies ⋮ A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets