Automatic recognition of tractability in inference relations
From MaRDI portal
Publication:5286164
DOI10.1145/151261.151265zbMath0770.68106OpenAlexW1973745704MaRDI QIDQ5286164
Publication date: 29 June 1993
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1721.1/6528
automated reasoningproof theorypolynomial-time algorithmdeductionproof systemscomputational logicinference rulesmechanical verificationmechanical theorem provingmachine inference
Related Items
The Complexity of Disjunction in Intuitionistic Logic, Interpolation systems for ground proofs in automated deduction: a survey, Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks, Intruder deduction for the equational theory of abelian groups with distributive encryption, Modular proof systems for partial functions with Evans equality, Deducibility constraints and blind signatures, Challenges in the Automated Verification of Security Protocols, Efficient representation of the attacker's knowledge in cryptographic protocols analysis, Intruder deducibility constraints with negation. Decidability and application to secured service compositions, Intruder deduction problem for locally stable theories with normal forms and inverses, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, From Search to Computation: Redundancy Criteria and Simplification at Work, Constructing Bachmair-Ganzinger Models, On Combinations of Local Theory Extensions, Symbolic protocol analysis for monoidal equational theories, Hierarchical combination of intruder theories, Automatic decidability and combinability, On Hierarchical Reasoning in Combinations of Theories, On Local Reasoning in Verification, On Interpolation and Symbol Elimination in Theory Extensions, Deciding knowledge in security protocols under some e-voting theories, A strong version of Herbrand's theorem for introvert sentences, Easy intruder deduction problems with homomorphisms, Algorithms and reductions for rewriting problems. II., EXPLORING THE LANDSCAPE OF RELATIONAL SYLLOGISTIC LOGICS
