Switch to: References

Add citations

You must login to add citations.
  1. Turning decision procedures into disprovers.André Rognes - 2009 - Mathematical Logic Quarterly 55 (1):87-104.
    A class of many-sorted polyadic set algebras is introduced. These generalise structure and model in a way that is relevant in regards to the Entscheidungsproblem and to automated reasoning.A downward Löwenheim-Skolem property is shown in that each satisfiable finite conjunction of purely relational first-order prenex sentences has a finite generalised model. This property does, together with a construction related to doubling the size of a finite structure, provide several strict generalisations of the strategy of finite model search for disproving.
    Direct download  
     
    Export citation  
     
    Bookmark  
  • Undecidability results on two-variable logics.Erich Grädel, Martin Otto & Eric Rosen - 1999 - Archive for Mathematical Logic 38 (4-5):313-354.
    It is a classical result of Mortimer that $L^2$ , first-order logic with two variables, is decidable for satisfiability. We show that going beyond $L^2$ by adding any one of the following leads to an undecidable logic:– very weak forms of recursion, viz.¶(i) transitive closure operations¶(ii) (restricted) monadic fixed-point operations¶– weak access to cardinalities, through the Härtig (or equicardinality) quantifier¶– a choice construct known as Hilbert's $\epsilon$ -operator.In fact all these extensions of $L^2$ prove to be undecidable both for satisfiability, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  • Dominoes and the complexity of subclasses of logical theories.Erich Grädel - 1989 - Annals of Pure and Applied Logic 43 (1):1-30.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations