scientific article; zbMATH DE number 1110839

MaRDI QIDQ4375199zbMATH OpenFDO

Authors Margus Veanes

Publication date 28 January 1998

zbMATH Keywords

automated theorem proving methodsHerbrand Skeleton problem

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Recommendations

• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• The decidability of simultaneous rigid E-unification with one variable
• The undecidability of simultaneous rigid E-unification with two variables
• The undecidability of simultaneous rigid E-unification
• Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification

Cited in

(14)

• Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
• E-unification for subsystems of S4
• The decidability of simultaneous rigid E-unification with one variable
• The undecidability of simultaneous rigid E-unification with two variables
• scientific article; zbMATH DE number 2044516 (Why is no real title available?)
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• RIGID REACHABILITY, THE NON-SYMMETRIC FORM OF RIGID E-UNIFICATION
• Simultaneous rigid E-unification is undecidable
• The undecidability of simultaneous rigid E-unification
• Complexity of the opacity algorithm in document-centric workflow systems
• Nondeterministic tree-walking automata are not closed under complementation
• Restricted unification in the DL \(\mathcal{FL}_0\)

This page was built for publication:

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