Automatic recognition of tractability in inference relations

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

zbMATH Keywords

automated reasoning proof theory polynomial-time algorithm deduction proof systems computational logic inference rules mechanical verification mechanical theorem proving machine inference

Mathematics Subject Classification ID

Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).

Related Items (25)

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

This page was built for publication: Automatic recognition of tractability in inference relations