8
$\begingroup$

When the site was proposed the name Proof Assistants was given (ref). However in the unofficial chat room, Area 51 meta questions and other places it became clear that others wanted the site to be about more than just proof assistants (ref).

One word that encompasses more of what others seek yet still tracks with the needs is Computational Logic.

I am still seeking a word or phrase that is includes more but this works for me at present.

For those wondering if a SE site can change its name and URL once it has entered beta, Yes. (ref 1) (ref 2)

Should questions arising from computational logic be asked?

$\endgroup$
2
  • $\begingroup$ Do you mean "computational logic"? Then be prepared for questions about SAT solvers, and this is likely very popular, but rather orthogonal to proof assistants, topic. $\endgroup$
    – Dima Pasechnik
    Commented Feb 9, 2022 at 13:13
  • $\begingroup$ IMHO most SAT solving people have quite orthogonal interests, for it's closer to areas such as combinatorial optimisation and HPC than to proof assistants proper. $\endgroup$
    – Dima Pasechnik
    Commented Feb 10, 2022 at 9:51

3 Answers 3

Reset to default
7
$\begingroup$

Paulson defines the term as:

Computational logic is concerned with formal logic as implemented on computers, where it is frequently applied to solve problems related to computation.

This seems very much "on topic" for this stackexchange.

$\endgroup$
6
$\begingroup$

Miller, [2017] "Using linear logic and proof theory to unify computational logic" lists the following topics as constituents of computational logic:

  • Logic programming (proof search)
  • Term representation
  • Type systems (Curry-Howard)
  • Functional programming (proof normalization)
  • Model checking
  • Theorem proving in logic and arithmetic, both automatic and interactive

So I guess it could be regarded as a common theory for both proof assistants and model checkers.

$\endgroup$
2
$\begingroup$

I think it's too broad, as a large part of computational logic is about HPC (High Performance Computing) on easy to formalise and encode (for computer input) problems such as SAT, whereas the intention of this site is to focus on problems which have much more to do with problems which are hard to formalise, and one has to go to great depths of theory and practice to achieve such formalisation (and encoding).

$\endgroup$
1
  • $\begingroup$ I was going to post that "sometimes less is more," meaning that the phrase "proof assistants" is narrower than the Communities actual interests but helpful to focus the (collective) mind. $\endgroup$
    – hardmath
    Commented Feb 28, 2022 at 18:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .