Partager via

Research: What is Automated Reasoning

 

If we are going to discuss software engineering over time, then we got to start with the basics.  The reference for this is at:

https://combination.cs.uiowa.edu/

  • Combination of logics (e.g., modal logics, logics in AI, ...);
  • Combination of constraint solving techniques (unification and matching algorithms, general symbolic constraints, numerical constraints, ...) and combination of decision procedures;
  • Integration of equational and other theories into deductive systems (e.g. theory resolution, constraint resolution, constraint paramodulation, ...);
  • Combination of term rewriting systems;
  • Integration of data structures (e.g., sets, multisets, lists) into CLP formalisms and deduction processes;
  • Hybrid systems in computational linguistics, knowledge representation, natural language semantics, and human computer interaction;
  • Logic modelling of multi-agent systems.

Speaking of agents, let’s have Marvin talk a little about Automated Reasoning, then examples are below the discussion, for translation purposes all of the discussion is included in the article, except for the jokes, which I doubt translate well:

 

To understand the format of the input tools:

Example of Automated Reasoning using the SMT process provided online by Microsoft Research:

It is fairly easy to write a SMT theorem that is will return SAT, and there are many examples, but what will cause an UNSAT?

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)

(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(assert (<= (* 2 c) (- b 8)))
(check-sat)