ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Electronic Resource
    Electronic Resource
    Commodious Axiomatization of Quantifiers in Multiple-Valued Logic (1998)
    Springer
    Studia logica 61 (1998), S. 101-121 
    Details
    ISSN: 1572-8730
    Keywords: many-valued logic ; infinitely-valued logic ; distribution quantifiers ; distributive lattices ; semantic tableaux ; sequent calculi
    Source: Springer Online Journal Archives 1860-2000
    Topics: Mathematics , Philosophy
    Notes: Abstract We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation theorem for finite distributive lattices are used to derive tableau-style axiomatizations of distribution quantifiers.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005086415447
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    Many-valued logic and mixed integer programming (1994)
    Springer
    Annals of mathematics and artificial intelligence 12 (1994), S. 231-263 
    Details
    ISSN: 1573-7470
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics
    Notes: Abstract We generalize prepositional semantic tableaux for classical and many-valued logics toconstraint tableaux. We show that this technique is a generalization of the standard translation from CNF formulas into integer programming. The main advantages are (i) a relatively efficient satisfiability checking procedure for classical, finitely-valued and, for the first time, for a wide range of infinitely-valued propositional logics; (ii) easy NP-containment proofs for many-valued logics. The standard translation of two-valued CNF formulas into integer programs and Tseitin's structure preserving clause form translation are obtained as a special case of our approach.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01530787
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    Fast Subsumption Checks Using Anti-Links (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 47-83 
    Details
    ISSN: 1573-0670
    Keywords: subsumption ; anti-links
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The concept of anti-link is defined (an anti-link consists of two occurrences of the same literal in a formula), and useful equivalence-preserving operations based on anti-links are introduced. These operations eliminate a potentially large number of subsumed paths in a negation normal form formula. Those anti-links that directly indicate the presence of subsumed paths are characterized. The operations have linear time complexity in the size of that part of the formula containing the anti-link. The problem of removing all subsumed paths in an NNF formula is shown to be NP-hard, even though such formulas may be small relative to the size of their path sets. The general problem of determining whether there exists a pair of subsumed paths associated with an arbitrary anti-link is shown to be NP-complete. Additional techniques that generalize the concept of pure literals are introduced and are also shown to eliminate redundant subsumption checks. The effectiveness of these techniques is examined with respect to some benchmark examples from the literature.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005711712356
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    The liberalized δ-rule in free variable semantic tableaux (1994)
    Springer
    Journal of automated reasoning 13 (1994), S. 211-221 
    Details
    ISSN: 1573-0670
    Keywords: Mechanical theorem proving ; tableau calculus
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract In this paper we have a closer look at one of the rules of the tableau calculus presented by Fitting [4], called the δ-rule. We prove that a modification of this rule, called the δ+-rule, which uses fewer free variables, is also sound and complete. We examine the relationship between the δ+-rule and variations of the δ-rule presented by Smullyan [9]. This leads to a second proof of the soundness of the δ+-rule. An example shows the relevance of this modification for building tableau-based theorem provers.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00881956
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 5
    facet.materialart.
    Unknown
    Short Conjunctive Normal Forms in Finitely Valued Logics (1994)
    Oxford University Press
    Details
    Publication Date: 1994-01-01
    Print ISSN: 0955-792X
    Electronic ISSN: 1465-363X
    Topics: Computer Science , Mathematics
    Published by Oxford University Press
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    PAPER CURRENT
  • 6
    facet.materialart.
    Unknown
    Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages (2005)
    Oxford University Press
    Details
    Publication Date: 2005-07-01
    Print ISSN: 1367-0751
    Electronic ISSN: 1368-9894
    Topics: Mathematics
    Published by Oxford University Press
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    PAPER CURRENT
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...