thumb|200px|A graphical representation of a partially built propositional tableau In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics (Girle 2000). An analytic tableau has for each node a subformula of the formula at the origin.

PropertyValue
dbpedia-owl:thumbnail
dbpprop:abstract
  • thumb|200px|A graphical representation of a partially built propositional tableau In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics (Girle 2000). An analytic tableau has for each node a subformula of the formula at the origin. In other words, it is a tableau satisfying the subformula property.
  • Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Evert Willem BethBeth-Kalküle genannt, sind stark Semantiksemantisch motivierte WiderlegungsverfahrenWiderlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments beweisen, sondern die dessen Ungültigkeit widerlegen; ein anderer, sehr bekannter Widerlegungskalkül ist der Resolution (Logik)Resolutionskalkül. Der Name „Baumkalkül“ rührt daher, dass beim Ableiten in einem Beth-Kalkül eine Baumstruktur erzeugt wird. Diese Aussage ist eine Beschreibung, keine Definition, weil nicht jeder Kalkül, der Baumstrukturen erzeugt, auch Baumkalkül genannt wird. Die entstandenen Baumstrukturen werden auch Beth-Tableaux oder Beth-Tableaus (französischer bzw. eingedeutschter Plural von Beth-Tableau) genannt. In diesem Artikel soll ein Baumkalkül für die klassische Aussagenlogik vorgestellt werden: Ein Kalkül für die Klassische Logikklassische Logik deshalb, weil die historisch ersten Baumkalküle klassisch waren; ein Kalkül für die Aussagenlogik deshalb, weil dieser der einfachste ist und die Grundlage vieler anderer Baumkalküle bildet, zunächst für den Baumkalkül der wichtigen klassischen Prädikatenlogik. Tableaukalküle gibt es auch für viele nichtklassische logische Systeme.
  • Een semantisch tableau is een manier om in de logica (wetenschap)logica op systematische wijze het gedrag van een logische stelling of formule te onderzoeken. Semantische tableaus worden vooral gebruikt om te onderzoeken of een stelling volgt uit een reeks andere stellingen, dat wil zeggen of een stelling per definitie waar is, gegeven dat een aantal andere stelling waar is. Onder het kopje [#bewijs uit het ongerijmde] wordt dit verder toegelicht. Het semantisch tableau is een schepping van de Nederlandse logicus Evert Willem Beth.
dbpprop:hasPhotoCollection
dbpprop:reference
rdfs:comment
  • thumb|200px|A graphical representation of a partially built propositional tableau In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics (Girle 2000). An analytic tableau has for each node a subformula of the formula at the origin.
  • Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Evert Willem BethBeth-Kalküle genannt, sind stark Semantiksemantisch motivierte WiderlegungsverfahrenWiderlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments beweisen, sondern die dessen Ungültigkeit widerlegen; ein anderer, sehr bekannter Widerlegungskalkül ist der Resolution (Logik)Resolutionskalkül.
  • Een semantisch tableau is een manier om in de logica (wetenschap)logica op systematische wijze het gedrag van een logische stelling of formule te onderzoeken. Semantische tableaus worden vooral gebruikt om te onderzoeken of een stelling volgt uit een reeks andere stellingen, dat wil zeggen of een stelling per definitie waar is, gegeven dat een aantal andere stelling waar is. Onder het kopje [#bewijs uit het ongerijmde] wordt dit verder toegelicht.
rdfs:label
  • Method of analytic tableaux
  • Baumkalkül
  • Semantisch tableau
owl:sameAs
skos:subject
foaf:depiction
foaf:page
is dbpprop:disambiguates of
is dbpprop:redirect of