Automatic recognition of tractability in inference relations

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

Mathematics Subject Classification ID

Recommendations

Polynomial-time computation via local inference relations
Tractable inference systems: an extension with a deducibility predicate
Reasoning about set constraints applied to tractable inference in intuitionistic logic
On some tractable classes in deduction and abduction
Taxonomic syntax for first order inference

Cited in

(32)

Easy intruder deduction problems with homomorphisms
Controlling recursive inference
Algorithms and reductions for rewriting problems. II.
Modular proof systems for partial functions with Evans equality
Symbolic protocol analysis for monoidal equational theories
Hierarchical combination of intruder theories
Interpolation systems for ground proofs in automated deduction: a survey
Deciding knowledge in security protocols under some e-voting theories
Decidability, introduction rules and automata
Challenges in the Automated Verification of Security Protocols
A strong version of Herbrand's theorem for introvert sentences
Reasoning about set constraints applied to tractable inference in intuitionistic logic
Deducibility constraints and blind signatures
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
Tractable inference systems: an extension with a deducibility predicate
Exploring the landscape of relational syllogistic logics
Intruder deducibility constraints with negation. Decidability and application to secured service compositions
The complexity of disjunction in intuitionistic logic
On Local Reasoning in Verification
Automatic decidability and combinability
On Hierarchical Reasoning in Combinations of Theories
On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $$\mathcal{E}\mathcal{L}, \mathcal{E}\mathcal{L}^+$$
Equivalence checking for orthocomplemented bisemilattices in log-linear time
Intruder deduction problem for locally stable theories with normal forms and inverses
Relatively complete and efficient partial quantifier elimination
On symbol elimination and uniform interpolation in theory extensions
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
Efficient representation of the attacker's knowledge in cryptographic protocols analysis

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5286164)