This HTML5 document contains 72 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dcthttp://purl.org/dc/terms/
yago-reshttp://yago-knowledge.org/resource/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n8http://dbpedia.org/resource/File:
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n12http://en.wikipedia.org/wiki/
dbchttp://dbpedia.org/resource/Category:
provhttp://www.w3.org/ns/prov#
dbphttp://dbpedia.org/property/
xsdhhttp://www.w3.org/2001/XMLSchema#
goldhttp://purl.org/linguistics/gold/
dbrhttp://dbpedia.org/resource/

Statements

Subject Item
dbr:Method_of_analytic_tableaux
rdf:type
dbo:AnatomicalStructure
rdfs:label
Method of analytic tableaux
rdfs:comment
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).
owl:sameAs
yago-res:Method_of_analytic_tableaux freebase:m.03_hjg
dbp:wikiPageUsesTemplate
dbt:IPAc-en dbt:Reflist
dct:subject
dbc:Automated_theorem_proving dbc:Logical_calculi dbc:Methods_of_proof
gold:hypernym
dbr:Procedure
prov:wasDerivedFrom
n12:Method_of_analytic_tableaux?oldid=1017796822&ns=0
dbo:wikiPageID
1027229
dbo:wikiPageLength
70336
dbo:wikiPageRevisionID
1017796822
dbo:wikiPageWikiLink
dbr:Structural_proof_theory dbr:T_(modal_logic) dbr:Richard_Jeffrey dbr:Quantifier_(logic) dbr:Logical_truth dbr:Contradiction dbr:Truth_value dbr:S5_(modal_logic) dbr:Formula dbr:Evert_Willem_Beth dbr:Iterative_deepening_depth-first_search n8:First-order_tableau_with_unification.svg dbr:Material_conditional n8:Prop-tableau-4.svg n8:Non-closed_propositional_tableau.svg dbr:Walter_Carnielli n8:Partially_built_tableau.svg dbr:De_Morgan's_laws dbr:Atomic_formula dbr:Classical_logic dbr:Set_(mathematics) dbr:Skolem_normal_form dbr:Tree_(data_structure) dbr:Resolution_(logic) n8:Prop-tableau-1.svg dbr:Handbook_of_Automated_Reasoning dbr:Cut-elimination_theorem dbr:Tautology_(logic) n8:Prop-tableau-2.svg n8:Prop-tableau-3.svg n8:Search_tree_of_tableau_space.svg dbr:Modal_logic dbr:Decision_problem dbr:Raymond_Smullyan dbr:Logical_consequence dbr:Propositional_calculus dbr:Satisfiability dbr:First-order_logic dbc:Methods_of_proof dbr:Multiset dbr:Logical_connective dbr:Negation_normal_form n8:First-order_tableau.svg dbr:Semantics dbr:K_(modal_logic) dbr:Sequent_calculus dbr:Clause_(logic) dbr:Proof_procedure dbr:Lewis_Carroll dbr:Logical_equivalence dbr:Ground_expression dbc:Automated_theorem_proving dbr:Proof_theory dbr:List_(abstract_data_type) dbc:Logical_calculi
dbo:abstract
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).
foaf:isPrimaryTopicOf
n12:Method_of_analytic_tableaux