| http://dbpedia.org/ontology/abstract
|
Na teoria da prova, o tableau semântico (p … Na teoria da prova, o tableau semântico (pronúncia em francês: [ta'blo]; singular: tableau; plural: tableaux), também chamado de árvore verdade, é um sistema de dedução para resolver problemas de decisão na lógica proposicional e outras relacionadas, e um para fórmulas da lógica de primeira ordem. O método de tableau também pode determinar a satisfatibilidade para conjuntos finitos de fórmulas de várias lógicas. É o mais popular para a lógica modal (Girle 2000), além de adequado para implementações em computadores. O método dos tableaux semântico foi inventada pelo lógico holandês Evert Willem Beth (Beth 1955), e, de forma independente, pelo lógico finlandês Jaakko Hintikka, foi simplificado para a lógica clássica por Raymond Smullyan (Smullyan 1968, 1995). A simplificação de Smullyan, "one-sided tableaux", é descrito a seguir. O método de Smullyan foi generalizado para arbitrárias lógicas proposicionais polivalentes e de primeira ordem por Walter Carnielli (Carnielli 1987). O tableaux pode ser intuitivamente visto como o método de sequentes de cima para baixo. Esta relação simétrica entre o tableaux e o cálculo de sequentes foi formalmente estabelecido por Carnielli (1991). Um tableau analítica tem, para cada nó, um subformula da fórmula na origem. Em outras palavras, é um tableau que satisfaz a propriedade da subformula. que satisfaz a propriedade da subformula.
, El método de las tablas semánticas, presen … El método de las tablas semánticas, presentado por E. Beth y popularizado como árboles semánticos por R. Smullyan, consiste básicamente en examinar, de manera sistemática, todas las posibilidades que podrían hacer falsa una proposición dada y buscar si una de estas posibilidades es lógicamente viable. Un árbol semántico es una sucesión de sucesiones de fórmulas llamadas ramas, generadas a partir de un conjunto (no vacío) de fórmulas, por aplicación a éstas de las reglas (y a las fórmulas resultantes que sean complejas). fórmulas resultantes que sean complejas).
, En théorie de la démonstration, les tablea … En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000). Elle fut inventée par le logicien hollandais Evert Willem Beth. le logicien hollandais Evert Willem Beth.
, In proof theory, the semantic tableau (/tæ … In proof theory, the semantic tableau (/tæˈbloʊ, ˈtæbloʊ/; plural: tableaux, also called truth tree) is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. 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).f procedure for modal logics (Girle 2000).
, Een semantisch tableau is een grafische we … Een semantisch tableau is een grafische weergave van een manier om in de 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 waar is, gegeven dat een aantal andere stellingen waar zijn. Het semantisch tableau is een schepping van de Nederlandse logicus Evert Willem Beth. de Nederlandse logicus Evert Willem Beth.
, Tableau (l. mn. tableaux) – system automat … Tableau (l. mn. tableaux) – system automatycznego dowodzenia twierdzeńpolegający na konstruowaniu „drzewa” – w jego korzeniu umieszczamy formułę, której sprzeczność chcemy wykazać, mianowicie zaprzeczenie formuły, której tautologiczność chcemy wykazać. Następnie na końcu dowolnej „gałęzi”:
* jeśli w jakimkolwiek miejscu „gałęzi” mamy możemy dodać
* jeżeli w „gałęzi” znajduje się możemy umieścić a pod nim
* gdy w pewnej części „gałęzi” jest możemy wstawić rozgałęzienie: z jednej strony, z drugiej,
* ...,
* itd., w zależności od logiki. Jeśli w dowolnej „gałęzi”, dla dowolnego jest jednocześnie i oznacza to, iż otrzymaliśmy sprzeczność i gałąź ta jest zamknięta, a więc możemy pominąć tę gałąź w dalszych rozważaniach. Jeśli zamknęliśmy wszystkie gałęzie, oznacza to, że dana formuła jest sprzeczna.znacza to, że dana formuła jest sprzeczna.
, Baumkalküle oder Tableaukalküle, nach ihre … Baumkalküle oder Tableaukalküle, nach ihrem Erfinder auch Beth-Kalküle genannt, sind Widerlegungskalküle der Logik. 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.utschter Plural von Beth-Tableau) genannt.
, タブローの方法(英 tableau method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。ヤーッコ・ヒンティッカらのという考え方を応用して作られ、レイモンド・スマリヤンによって広められた。
|
| http://dbpedia.org/ontology/thumbnail
|
http://commons.wikimedia.org/wiki/Special:FilePath/Partially_built_tableau.svg?width=300 +
|
| http://dbpedia.org/ontology/wikiPageExternalLink
|
http://hackage.haskell.org/package/tableaux +
, https://philpapers.org/rec/BETSEA-10 +
, http://www.irit.fr/Lotrec/ +
, http://i12www.ira.uka.de/TABLEAUX/ +
, http://www.clas.ufl.edu/users/jzeman/modallogic/ +
, http://www.umsu.de/logik/trees/ +
, https://www.springer.com/computer/theoretical%2Bcomputer%2Bscience/journal/10817 +
|
| http://dbpedia.org/ontology/wikiPageID
|
1027229
|
| http://dbpedia.org/ontology/wikiPageLength
|
72648
|
| http://dbpedia.org/ontology/wikiPageRevisionID
|
1115819739
|
| http://dbpedia.org/ontology/wikiPageWikiLink
|
http://dbpedia.org/resource/Ground_term +
, http://dbpedia.org/resource/Logical_truth +
, http://dbpedia.org/resource/Modal_logic +
, http://dbpedia.org/resource/Material_conditional +
, http://dbpedia.org/resource/Tree_%28data_structure%29 +
, http://dbpedia.org/resource/First-order_predicate_logic +
, http://dbpedia.org/resource/Resolution_%28logic%29 +
, http://dbpedia.org/resource/Tautology_%28logic%29 +
, http://dbpedia.org/resource/Raymond_Smullyan +
, http://dbpedia.org/resource/Logical_connective +
, http://dbpedia.org/resource/Cut-elimination_theorem +
, http://dbpedia.org/resource/Structural_proof_theory +
, http://dbpedia.org/resource/Contradiction +
, http://dbpedia.org/resource/First-order_logic +
, http://dbpedia.org/resource/Proof_theory +
, http://dbpedia.org/resource/Negation_normal_form +
, http://dbpedia.org/resource/Iterative_deepening +
, http://dbpedia.org/resource/Category:Methods_of_proof +
, http://dbpedia.org/resource/Kripke_semantics +
, http://dbpedia.org/resource/Skolem_term +
, http://dbpedia.org/resource/Many-valued_logic +
, http://dbpedia.org/resource/File:Prop-tableau-4.svg +
, http://dbpedia.org/resource/File:Prop-tableau-2.svg +
, http://dbpedia.org/resource/File:Prop-tableau-3.svg +
, http://dbpedia.org/resource/File:Prop-tableau-1.svg +
, http://dbpedia.org/resource/Classical_logic +
, http://dbpedia.org/resource/Skolem_normal_form +
, http://dbpedia.org/resource/Propositional_logic +
, http://dbpedia.org/resource/Proof_procedure +
, http://dbpedia.org/resource/Category:Automated_theorem_proving +
, http://dbpedia.org/resource/K_%28modal_logic%29 +
, http://dbpedia.org/resource/File:Search_tree_of_tableau_space.svg +
, http://dbpedia.org/resource/Set_%28mathematics%29 +
, http://dbpedia.org/resource/Atom_%28logic%29 +
, http://dbpedia.org/resource/Multiset +
, http://dbpedia.org/resource/File:Partially_built_tableau.svg +
, http://dbpedia.org/resource/File:Non-closed_propositional_tableau.svg +
, http://dbpedia.org/resource/T_%28modal_logic%29 +
, http://dbpedia.org/resource/File:First-order_tableau.svg +
, http://dbpedia.org/resource/Atomic_formula +
, http://dbpedia.org/resource/Sentential_logic +
, http://dbpedia.org/resource/S5_%28modal_logic%29 +
, http://dbpedia.org/resource/Formula +
, http://dbpedia.org/resource/Semantics +
, http://dbpedia.org/resource/Charles_Lutwidge_Dodgson +
, http://dbpedia.org/resource/Quantifier_%28logic%29 +
, http://dbpedia.org/resource/Decision_procedure +
, http://dbpedia.org/resource/List_%28computing%29 +
, http://dbpedia.org/resource/Truth_value +
, http://dbpedia.org/resource/Satisfiable +
, http://dbpedia.org/resource/Entailment +
, http://dbpedia.org/resource/Walter_Carnielli +
, http://dbpedia.org/resource/De_Morgan%27s_laws +
, http://dbpedia.org/resource/Polynomial_space +
, http://dbpedia.org/resource/Logical_consequence +
, http://dbpedia.org/resource/Clause_%28logic%29 +
, http://dbpedia.org/resource/Sequent_calculus +
, http://dbpedia.org/resource/Satisfiability +
, http://dbpedia.org/resource/File:First-order_tableau_with_unification.svg +
, http://dbpedia.org/resource/Category:Logical_calculi +
, http://dbpedia.org/resource/Connective_%28logic%29 +
, http://dbpedia.org/resource/Evert_Willem_Beth +
, http://dbpedia.org/resource/Logically_equivalent +
|
| http://dbpedia.org/property/wikiPageUsesTemplate
|
http://dbpedia.org/resource/Template:GBurl +
, http://dbpedia.org/resource/Template:Harvid +
, http://dbpedia.org/resource/Template:Cite_journal +
, http://dbpedia.org/resource/Template:Cite_book +
, http://dbpedia.org/resource/Template:Reflist +
, http://dbpedia.org/resource/Template:IPAc-en +
, http://dbpedia.org/resource/Template:Harvnb +
|
| http://purl.org/dc/terms/subject
|
http://dbpedia.org/resource/Category:Automated_theorem_proving +
, http://dbpedia.org/resource/Category:Methods_of_proof +
, http://dbpedia.org/resource/Category:Logical_calculi +
|
| http://purl.org/linguistics/gold/hypernym
|
http://dbpedia.org/resource/Procedure +
|
| http://www.w3.org/ns/prov#wasDerivedFrom
|
http://en.wikipedia.org/wiki/Method_of_analytic_tableaux?oldid=1115819739&ns=0 +
|
| http://xmlns.com/foaf/0.1/depiction
|
http://commons.wikimedia.org/wiki/Special:FilePath/Non-closed_propositional_tableau.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Prop-tableau-4.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/First-order_tableau.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/First-order_tableau_with_unification.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Prop-tableau-2.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Prop-tableau-3.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Prop-tableau-1.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Partially_built_tableau.svg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Search_tree_of_tableau_space.svg +
|
| http://xmlns.com/foaf/0.1/isPrimaryTopicOf
|
http://en.wikipedia.org/wiki/Method_of_analytic_tableaux +
|
| owl:sameAs |
http://pl.dbpedia.org/resource/Tableau_%28system_dowodzenia_twierdze%C5%84%29 +
, http://nl.dbpedia.org/resource/Semantisch_tableau +
, http://pt.dbpedia.org/resource/M%C3%A9todo_dos_Tableaux_Anal%C3%ADticos +
, http://dbpedia.org/resource/Method_of_analytic_tableaux +
, https://global.dbpedia.org/id/4y6cF +
, http://es.dbpedia.org/resource/%C3%81rbol_sem%C3%A1ntico +
, http://yago-knowledge.org/resource/Method_of_analytic_tableaux +
, http://fr.dbpedia.org/resource/M%C3%A9thode_des_tableaux +
, http://www.wikidata.org/entity/Q811591 +
, http://de.dbpedia.org/resource/Baumkalk%C3%BCl +
, http://rdf.freebase.com/ns/m.03_hjg +
, http://ja.dbpedia.org/resource/%E3%82%BF%E3%83%96%E3%83%AD%E3%83%BC%E3%81%AE%E6%96%B9%E6%B3%95 +
|
| rdf:type |
http://dbpedia.org/class/yago/Ability105616246 +
, http://dbpedia.org/class/yago/PsychologicalFeature100023100 +
, http://dbpedia.org/class/yago/Cognition100023271 +
, http://dbpedia.org/ontology/AnatomicalStructure +
, http://dbpedia.org/class/yago/Abstraction100002137 +
, http://dbpedia.org/class/yago/Know-how105616786 +
, http://dbpedia.org/class/yago/Method105660268 +
, http://dbpedia.org/class/yago/WikicatMethodsOfProof +
|
| rdfs:comment |
Een semantisch tableau is een grafische we … Een semantisch tableau is een grafische weergave van een manier om in de 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 waar is, gegeven dat een aantal andere stellingen waar zijn. Het semantisch tableau is een schepping van de Nederlandse logicus Evert Willem Beth. de Nederlandse logicus Evert Willem Beth.
, タブローの方法(英 tableau method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。ヤーッコ・ヒンティッカらのという考え方を応用して作られ、レイモンド・スマリヤンによって広められた。
, Na teoria da prova, o tableau semântico (p … Na teoria da prova, o tableau semântico (pronúncia em francês: [ta'blo]; singular: tableau; plural: tableaux), também chamado de árvore verdade, é um sistema de dedução para resolver problemas de decisão na lógica proposicional e outras relacionadas, e um para fórmulas da lógica de primeira ordem. O método de tableau também pode determinar a satisfatibilidade para conjuntos finitos de fórmulas de várias lógicas. É o mais popular para a lógica modal (Girle 2000), além de adequado para implementações em computadores. O método dos tableaux semântico foi inventada pelo lógico holandês Evert Willem Beth (Beth 1955), e, de forma independente, pelo lógico finlandês Jaakko Hintikka, foi simplificado para a lógica clássica por Raymond Smullyan (Smullyan 1968, 1995). A simplificação de Smullyan, 1968, 1995). A simplificação de Smullyan,
, In proof theory, the semantic tableau (/tæ … In proof theory, the semantic tableau (/tæˈbloʊ, ˈtæbloʊ/; plural: tableaux, also called truth tree) is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. 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).f procedure for modal logics (Girle 2000).
, Baumkalküle oder Tableaukalküle, nach ihre … Baumkalküle oder Tableaukalküle, nach ihrem Erfinder auch Beth-Kalküle genannt, sind Widerlegungskalküle der Logik. 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.utschter Plural von Beth-Tableau) genannt.
, En théorie de la démonstration, les tablea … En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000). Elle fut inventée par le logicien hollandais Evert Willem Beth. le logicien hollandais Evert Willem Beth.
, Tableau (l. mn. tableaux) – system automat … Tableau (l. mn. tableaux) – system automatycznego dowodzenia twierdzeńpolegający na konstruowaniu „drzewa” – w jego korzeniu umieszczamy formułę, której sprzeczność chcemy wykazać, mianowicie zaprzeczenie formuły, której tautologiczność chcemy wykazać. Następnie na końcu dowolnej „gałęzi”:
* jeśli w jakimkolwiek miejscu „gałęzi” mamy możemy dodać
* jeżeli w „gałęzi” znajduje się możemy umieścić a pod nim
* gdy w pewnej części „gałęzi” jest możemy wstawić rozgałęzienie: z jednej strony, z drugiej,
* ...,
* itd., w zależności od logiki.,
* ...,
* itd., w zależności od logiki.
, El método de las tablas semánticas, presen … El método de las tablas semánticas, presentado por E. Beth y popularizado como árboles semánticos por R. Smullyan, consiste básicamente en examinar, de manera sistemática, todas las posibilidades que podrían hacer falsa una proposición dada y buscar si una de estas posibilidades es lógicamente viable. Un árbol semántico es una sucesión de sucesiones de fórmulas llamadas ramas, generadas a partir de un conjunto (no vacío) de fórmulas, por aplicación a éstas de las reglas (y a las fórmulas resultantes que sean complejas). fórmulas resultantes que sean complejas).
|
| rdfs:label |
タブローの方法
, Baumkalkül
, Método dos Tableaux Analíticos
, Méthode des tableaux
, Semantisch tableau
, Method of analytic tableaux
, Árbol semántico
, Tableau (system dowodzenia twierdzeń)
|
