On quasitautologies

DOI10.1007/BFb0027417zbMath1415.03024MaRDI QIDQ4610330

Ján Komara, Paul J. Voda

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

automated theorem provingsubstitution ruleidentity rulefunction substitutionmain lemma

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items

Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The undecidability of simultaneous rigid E-unification
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• An algorithm for reasoning about equality
• On Shostak's decision procedure for combinations of theories
• Proof theory