First order Stålmarck. Universal lemmas through branch merges

DOI10.1007/s10817-008-9115-4zbMath1191.68618OpenAlexW1752750514WikidataQ125030637 ScholiaQ125030637MaRDI QIDQ1040785

Magnus Björk

Publication date: 25 November 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-008-9115-4

zbMATH Keywords

intersectionsautomated theorem provingfirst order logicStålmarck's methoduniversal lemmas

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (1)

Semantics and proof-theory of depth bounded Boolean logics

Uses Software

• OTTER
• TPTP
• E-SETHEO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library. CNF release v1. 2. 1
• Case study: Formal verification of a computerized railway interlocking
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• The model evolution calculus as a first-order DPLL method
• Proof and Model Generation with Disconnection Tableaux
• A Proof Method for Quantification Theory: Its Justification and Realization
• A First Order Extension of Stålmarck’s Method
• Automated Deduction – CADE-20
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Automated Deduction – CADE-19

This page was built for publication: First order Stålmarck. Universal lemmas through branch merges