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

[QPQ]

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

tinelli wrote at Jan 20, 2005 - 10:53 PM
---------------------------------------------------------------------

> "Logic" looks much better to me than "sublogic". All subfoos I know of 
> are foos themselves; they are just 'subfoos of' other foos.
> 
I agree.


> 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.
>
That would not work.
You do not want to put syntactical restrictions on the sentences in T. They should not be forced to be a subset of F.
For example for linear arithmetic T contains the axioms of the real closed fields. Those are more complex formulas than those allowed in F, which are instead boolean combination of linear (in)equations.

This is in general necessary because the language of F may be too weak to define the semantics (i.e. the allowed set of models) of the logic.
Think of difference logic. The language of difference constraints (boolean combination of atoms of the form x-y 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.
>
That is correct. Such a restriction was not intended. In a logic (T,L) T is a theory in the sense of the SMT-LIB document, which does not prescribe T to be axiomatizable.
T is just a set of sentences, however defined. The real purpose of T is to define a class of structures, namely the models of T, over which satisfiability modulo T is defined. (Recall that we define a formula to be T-satisfiable iff it is satisfied by one of the models of T).
Note that T could be equivalently defined in a completely semantical way, ie., directly as a class of structures. This is indeed the definition that some authors (including some in this forum) now use in their more recent work. I had proposed it at the very beginning of SMT-LIB a few years ago, but it did not gather much enthusiasm then. So we stuck to a view of theories as set of sentences.


 
> 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". 
>
Mmm. This does not seem to be well-defined. I think at the very least you need to assume that T and T' are deductively closed, that is, contain all of their logical consequences.


> 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?
> 
I think a more general definition of sublogic could the following:

(T,F) is a sublogic of (T',F') iff
a) the signature Sigma of (T,F) is included in the signature of (T',F'),
b) T entails all the Sigma-sentences entailed by T' and
c) F is a subset of F'.

In this sense,

- real arithmetic is a sublogic of trigonometry:
  it restricts the signature to the arithmetic symbols only;
- real arithmetic is a sublogic of (additive) commutative groups:
  its theory entails all the Abeliam group axioms over + and 0 and
  unary -.
- linear real arithmetic is a sublogic of non-linear real arithmetic:
  it restricts F to formulas with linear terms only;

Notice that here it is not the case that a decision procedure for the bigger logic is also a decision procedure for the smaller one (as the smaller one may have less models). I guess other sensible orderings are possible. But I do not think this is all that important for SMT-LIB anyway.



Cesare


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

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/