Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
From MaRDI portal
Publication:1960430
DOI10.1016/S0304-3975(98)00317-XzbMath0937.03020MaRDI QIDQ1960430
Publication date: 12 January 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items (3)
The undecidability of proof search when equality is a logical connective ⋮ Monadic simultaneous rigid \(E\)-unification ⋮ Decidability and complexity of simultaneous rigid E-unification with one variable and related results
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The undecidability of simultaneous rigid E-unification
- The undecidability of the second-order unification problem
- Extended universal theories of the integers
- 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
- Special cases and substitutes for rigid \(E\)-unification
- On the sequential nature of unification
- Parallel Algorithms for Term Matching
- On Matrices with Connections
- Contraction-free sequent calculi for intuitionistic logic
- Refutations by Matings
- The Diophantine Problem for Addition and Divisibility
- An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
- Decision procedures and model building in equational clause logic
- Monadic simultaneous rigid E-unification and related problems
- On quasitautologies
- Proof-search in intuitionistic logic based on constraint satisfaction
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
This page was built for publication: Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
