Turning decision procedures into disprovers
Copyright policy )Turning decision procedures into disprovers
AbstractA 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. (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)
Mechanization of proofs and logical operations, algebraic logic, Decidability of theories and sets of sentences, Cylindric and polyadic algebras; relation algebras, Entscheidungsproblem, polyadic set algebra, many-sorted polyadic algebra
Mechanization of proofs and logical operations, algebraic logic, Decidability of theories and sets of sentences, Cylindric and polyadic algebras; relation algebras, Entscheidungsproblem, polyadic set algebra, many-sorted polyadic algebra
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!