DOMAINS :: SMT-LIB :: Some SMT-COMP/LIB issues

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. Some SMT-COMP/LIB issues

savakrstic wrote at Jan 19, 2005 - 04:15 PM
---------------------------------------------------------------------
"Logic" looks much better to me than "sublogic". All subfoos I know of are foos themselves; they are just 'subfoos of' other foos. 

Regarding the definition of (sub)logic in this context as a pair (T,F) where F is a 
set of FOL formulas: in general, T could be required only to be a well-defined subset of F. It can be defined by means of a set of axioms, or as the set of F-formulas that are true in some particular model, or in some other way. Requiring only axiomatic definitions would probably be too restrictive. 

A natural ordering of our (sub)logics can be defined by "(T,F) < (T',F')  iff  F is a subset of F' and the intersection of T' with F is equal to T". Thus, a decision procedure for the bigger guy is a decision procedure for the smaller. Are there other useful orderings? Under which one is (empty_theory, all FOL formualae) the largest logic?  

Sava



---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=54&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=54

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/