About: Satisfiability modulo theories

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

Logical problem studied in computer science

Property	Value
dbo:description	logical problem studied in computer science (en) problema decisionale (it) логічна задача, що вивчається в інформатиці (uk)
dbo:wikiPageExternalLink	https://klee.github.io/ https://web.archive.org/web/20150406115407/https:/sites.google.com/site/stpfastprover/ https://github.com/Z3Prover/z3 http://alt-ergo.ocamlpro.com/ http://isat.gforge.avacs.org/ http://s2e.epfl.ch/ http://smt-lib.org/ http://smtlib.org/ http://www.smtcomp.org/ https://ucsd-progsys.github.io/liquidhaskell-blog/ https://z3string.github.io/ http://research.microsoft.com/en-us/projects/boogie/ http://research.microsoft.com/en-us/projects/chalice/ http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/fstar/ http://research.microsoft.com/en-us/projects/specsharp/ http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf https://sites.google.com/site/stpfastprover/ https://hackage.haskell.org/package/sbv https://kilthub.cmu.edu/articles/Microprocessor_Verification_Using_Efficient_Decision_Procedures_for_a_Logic_of_Equality_with_Uninterpreted_Functions/6607286/files/12097826.pdf https://ece.uwaterloo.ca/~vganesh/Publications_files/vg2007-PhD-STANFORD.pdf http://archive.sigda.org/newsletter/2006/061215.txt http://fmv.jku.at/boolector/ https://yurichev.com/writings/SAT_SMT_draft-EN.pdf http://www.satcompetition.org/2009/format-benchmarks2009.html http://vcc.codeplex.com http://viper.ethz.ch http://www.smtcomp.org https://triton.quarkslab.com https://books.google.com/books%3Fid=anJsH3Dq5BIC&q=SMT https://books.google.com/books%3Fid=shLvAgAAQBAJ&q=%22Satisfiability+Modulo+Theories%22 http://www.eecs.umich.edu/~karem http://www.sigda.org https://web.archive.org/web/20070208034716/http:/www.sigda.org/newsletter/index.html http://alt-ergo.lri.fr/documents/ABZ-2014.pdf http://cubicle.lri.fr/ http://why3.lri.fr/ https://www.easycrypt.info/
dbo:wikiPageWikiLink	dbr:Backtracking dbr:Transcendental_function dbr:Microsoft_Research dbr:Predicate_(mathematical_logic) dbr:AC_symbol dbc:SMT_solvers dbr:Difference_logic dbr:Enumerated_datatype dbr:Linear_arithmetic dbr:Polymorphic_array dbr:Record_datatype dbc:NP-complete_problems dbr:Constraint_satisfaction_problem dbr:Quantifier_elimination dbr:.NET_Framework dbr:C++ dbc:Electronic_design_automation dbr:Microprocessor dbr:Arms_control dbr:Quantifier_(logic) dbr:Modeling_language dbr:CeCILL-C dbr:Real_closed_field dbr:Arithmetic dbc:Formal_methods dbr:Real_number dbr:First-order_logic dbr:FreeBSD dbr:OpenBSD dbr:Program_synthesis dbr:Automated_theorem_proving dbr:Decidability_(logic) dbr:Atomic_formula dbr:Satisfiability dbr:Program_analysis dbc:Satisfiability_problems dbc:Logic_in_computer_science dbr:MIT_License dbr:Well-formed_formula dbr:Answer_set_programming dbr:OpenCog dbr:Java_(programming_language) dbr:Linux dbr:Microsoft_Windows dbr:BSD_licenses dbr:Logical_conjunction dbr:OCaml dbr:Interval_arithmetic dbr:Presburger_arithmetic dbr:Binary_data dbr:Inequality_(mathematics) dbr:GPLv3 dbr:Lazy_evaluation dbr:Data_structure dbr:Constraint_programming dbr:White-box_testing dbr:B-Method dbr:Theory_of_pure_equality dbr:C_(programming_language) dbr:Computer_science dbr:Computer_program dbr:Correctness_(computer_science) dbr:Scheme_(programming_language) dbr:Alfred_Tarski dbr:Boolean_satisfiability_problem dbr:Mathematical_logic dbr:DIMACS dbr:International_Joint_Conference_on_Automated_Reasoning dbr:Uninterpreted_function dbr:Relational_model dbr:Datapath dbr:Higher-order_logic dbr:Undecidable_problem dbr:Frama-C dbr:Formal_verification dbr:String_(computer_science) dbr:Affero_General_Public_License dbr:NP-hardness dbr:Python_(programming_language) dbc:Constraint_programming dbr:Type_inference dbr:S-expression dbr:DPLL_algorithm dbr:Atomic_sentence dbr:Rodin_tool dbr:SPARK_(programming_language) dbr:Symbolic_execution dbr:DPLL(T) dbr:Apache_license dbr:Common_Public_License dbr:Decision_problem dbr:Probabilistic_logic dbr:Computational_complexity dbr:Computer_Aided_Verification dbr:Concolic_testing dbr:Constraint_Handling_Rules dbr:Constraint_logic_programming dbr:Alt-Ergo dbr:Z3_Theorem_Prover dbr:Haskell_(programming_language) dbr:Theory_(mathematical_logic) dbr:LGPL dbr:OS_X dbr:Windows dbr:Array_data_structure dbr:Mac_OS dbr:List_(computing) dbr:Eager_evaluation dbr:Hardware_design dbr:LGPLv3 dbr:Free_theory dbr:Bit_vector dbr:Bit_vectors dbr:Congruence_closure dbr:Natural_numbers dbr:Real_numbers dbr:Empty_theory dbr:Uninterpreted_term dbr:Bitvector dbr:Integers
dbp:date	2015-04-06 (xsd:date)
dbp:url	https://web.archive.org/web/20150406115407/https:/sites.google.com/site/stpfastprover/
dbp:wikiPageUsesTemplate	dbt:Cite_book dbt:Abbr dbt:Anchor dbt:Cite_journal dbt:No dbt:Refend dbt:Yes dbt:Refbegin dbt:Citation_needed dbt:Mvar dbt:Visible_anchor dbt:Cite_thesis dbt:Mathematical_logic dbt:Webarchive dbt:Short_description
dct:subject	dbc:NP-complete_problems dbc:Electronic_design_automation dbc:Satisfiability_modulo_theories_solvers dbc:Formal_methods dbc:Satisfiability_problems dbc:Logic_in_computer_science dbc:Constraint_programming
gold:hypernym	dbr:Problem
rdfs:label	Satisfiability modulo theories (en) Teorías de satisfacibilidad módulo (es) Satisfiability modulo theories (fr) Задача выполнимости формул в теориях (ru) Satisfierbarhet modulo teorier (sv) Satisfiability Modulo Theories (uk)
owl:sameAs	freebase:Satisfiability modulo theories yago-res:Satisfiability modulo theories wikidata:Satisfiability modulo theories dbpedia-fr:Satisfiability modulo theories dbpedia-es:Satisfiability modulo theories dbpedia-hu:Satisfiability modulo theories dbpedia-fa:Satisfiability modulo theories dbpedia-ru:Satisfiability modulo theories dbpedia-sv:Satisfiability modulo theories dbpedia-hy:Satisfiability modulo theories dbpedia-uk:Satisfiability modulo theories dbpedia-global:Satisfiability modulo theories
prov:wasDerivedFrom	wikipedia-en:Satisfiability_modulo_theories?oldid=1291718120&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Satisfiability_modulo_theories
is dbo:knownFor of	dbr:Greg_Nelson_(computer_scientist)
is dbo:wikiPageDisambiguates of	dbr:SMT
is dbo:wikiPageRedirects of	dbr:Boolector dbr:CVC_theorem_prover dbr:Yices dbr:List_of_SMT_solvers dbr:Smt2_(file_format) dbr:CVC3 dbr:CVC4 dbr:CVC_(theorem_prover) dbr:CVC_Lite dbr:CVC_Lite_theorem_prover dbr:Satisfiability_Modulo_Theories dbr:Satisfiability_Modulo_Theories_problem dbr:SMT-LIB dbr:SMT_solver
is dbo:wikiPageWikiLink of	dbr:Greg_Nelson_(computer_scientist) dbr:Isabelle_(proof_assistant) dbr:Constraint_satisfaction_problem dbr:F*_(programming_language) dbr:Constraint_(mathematics) dbr:Superoptimization dbr:Proof_assistant dbr:Satisfiability dbr:Sentence_(mathematical_logic) dbr:OpenCog dbr:Extended_static_checking dbr:Fast_Fourier_transform dbr:Presburger_arithmetic dbr:SAT_solver dbr:List_of_programmers dbr:Boolector dbr:Boolean_satisfiability_problem dbr:E-graph dbr:Uninterpreted_function dbr:Entscheidungsproblem dbr:SMT dbr:Solver dbr:Formal_verification dbr:Vienna_Summer_of_Logic dbr:Predicate_transformer_semantics dbr:Type_inference dbr:Computer_algebra_system dbr:DPLL_algorithm dbr:Microsoft_and_open_source dbr:DPLL(T) dbr:List_of_computer_scientists dbr:Concolic_testing dbr:Alt-Ergo dbr:David_L._Dill dbr:Verve_(operating_system) dbr:Z3_Theorem_Prover dbr:Liquid_Haskell dbr:List_of_people_associated_with_PARC dbr:CVC_theorem_prover dbr:Maximum_satisfiability_problem dbr:Jose_Meseguer dbr:Constraint_satisfaction dbr:Matching_logic dbr:TLA+ dbr:Yices dbr:List_of_SMT_solvers dbr:Smt2_(file_format) dbr:CVC3 dbr:CVC4 dbr:CVC_(theorem_prover) dbr:CVC_Lite dbr:CVC_Lite_theorem_prover dbr:Satisfiability_Modulo_Theories dbr:Satisfiability_Modulo_Theories_problem dbr:SMT-LIB dbr:SMT_solver
is dbp:knownFor of	dbr:Greg_Nelson_(computer_scientist)
is rdfs:seeAlso of	dbr:Cooperating_Validity_Checker
is foaf:primaryTopic of	wikipedia-en:Satisfiability_modulo_theories