converting math problem into formal language question
in [Logic]
|
Prev: How can the MMx math be corrected?
Next: Is truth just something we have beliefs about or is there such a thing as truth?
From: Charlie-Boo on 3 Jun 2010 22:53 On Jun 1, 3:21 pm, George Greene <gree...(a)email.unc.edu> wrote: > On May 31, 2:01 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > AI people tried it for years - things like the Tower of Hanoi puzzle. > > Problem-Solving Methods in Artificial Intelligence, Nilsson, 1971. > > Chapter 7. Application of the Predicate Calculus in Problem Solving > > I do NOT think predicate calculus and a first-order "formal language" > are the kind of "formal language" that the OP had in mind. Why do you think that? > I think he was talking about a formal language as a set of strings > (individual strings of which might be accepted or rejected by a TM). Why doesn't predicate calculus fit that description? You have the set of wffs, the set of provable wffs, etc. all r.e. C-B
From: Charlie-Boo on 3 Jun 2010 23:04
On Jun 1, 4:55 pm, Xah Lee <xah...(a)gmail.com> wrote: > On Jun 1, 12:21 pm, George Greene <gree...(a)email.unc.edu> wrote: > > > On May 31, 2:01 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > AI people tried it for years - things like the Tower of Hanoi puzzle. > > > Problem-Solving Methods in Artificial Intelligence, Nilsson, 1971. > > > Chapter 7. Application of the Predicate Calculus in Problem Solving > > > I do NOT think predicate calculus and a first-order "formal language" > > are the kind of "formal language" that the OP had in mind. > > I think he was talking about a formal language as a set of strings > > (individual strings of which might be accepted or rejected by a TM). > > Yes George, that's correct. My goodness! Why doesn't Predicate Calculus qualify as an example of that last sentence? If you want to ignore the published literature, that is your perogative, To model winning a game, there is tons of literature on tree searches and pruning. AI may be exactly what you need here - your first specific problem. You have a game state and a function for each player that generates the next possible states (via a move), and an evaluation function as to which states are a win or lose for each of the 2 players. You need to define a winning state in terms of these functions and then prove that the starting state is one. In general, you need to walk through the possible situations encountered in solving a puzzle, and the model is the tree walk and optimizaion of the tree or its traversal. This is a very general model. C-B > Thanks for your input in previous post. > > Though, i hoped there's more input. I'm pretty sure this has been > explored. > > I'm rather not looking for a ad hoc solution to convert a particular > mathematical problem into formal language... but am more looking for > expert advices and materials... starting as a example, how to turn the > question whether it is possible to align 5 chess pieces in a chess > board. > > for example, there are lots of ways to turn a yes/no math problem into > yes/no question in formal language. So, some natural question arise... > which formal language is more efficient, how we judge, what are some > general tips and methods to convert math into formal language...etc. > (the goal i'm interested, is with respect to practical computability. > i.e. once the problem is changed into a formal language question, that > formal language should be easily implemented by computer, so that > massive computing power can churn out theorems brute-force in hope to > answer (Godel incompleteness theorems not withstanding... )) > > am looking for materials in this field. I'm pretty sure similar > question have been explored in automated math proof system > communities... > > am not professional mathematician or logician (am pro programer with > amateur expertise in math and logic). I've wrote something here that > may show why i'm interested in this: > > ⢠Math Notations, Computer Languages, and the âFormâ in Formalism >  http://xahlee.org/cmaci/notation/index.html > > > On May 31, 2:01 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > AI people tried it for years - things like the Tower of Hanoi puzzle. > > > Problem-Solving Methods in Artificial Intelligence, Nilsson, 1971. > > > Chapter 7. Application of the Predicate Calculus in Problem Solving > > cant find content or summary of that book or chapter online... is this > general AI or does it touches on the formal language in a technical > sense here? in any case, I'm sure today the field is quite different > from the perspectives of 1971... > > any automated/assisted theorem provers experts care to comment? > > part of the question is... this has a lot to do with one school of > math foundation, namely formalism and logicism. The ultimate goal is > to turn whole math into formal language of strings. I read a few > articles about theorem provers in 2008 > > ⢠State Of Theorem Proving Systems 2008 >  http://xahlee.org/cmaci/notation/theorem_proving_systems.html > > but haven't made my study far. I'm not sure, how these systems are > close to formal language of strings, but i think in is very close, or > perhaps modeled on the formal language of strings as much practical as > possible? > >  Xah > âhttp://xahlee.org/ > > â > > On May 21, 4:15 pm, George Greene <gree...(a)email.unc.edu> wrote: > > > > > On May 20, 4:13 pm, Xah Lee <xah...(a)gmail.com> wrote: > > > >  Modeling Math Problem Into a Question in Formal Language > > > Is this something that other people often do, > > or something that you are doing for the first time? > > > I personally have never seen a math problem modeled into "a question > > in" > > formal language. > > > Formal languages are sets of strings. > > The usual problem, in the context of ANY formal language, is simply > > to determine which strings belong to it and which do not. > > Please note that this DOES NOT involve any "question IN" the formal > > language. > > The formal language itself IS NOT a language IN WHICH "questions" > > can be phrased or posed, usually. > > > It simply contains [some] strings [and not others]. > > Usually, each of these strings would be thought of as a  STATEMENT or > > a (possible) > > SOLUTION to a problem, NOT A QUESTION. > > A string might also be a demonstration that a particular attempted > > solution fails. > > > One obvious way to translate THIS problem into a formal language would > > be to > > just model any/every game as the string of its moves.  But this would > > first > > require defining a finite alphabet for specifying moves.  For the n- > > angel problem, > > the king's moves are easy to define from an alphabet with n symbols > > since there > > are always at most (2n+1)^2 places to which the king could move (from > > where he was previously). > > But there is no upper bound on "where" a devil-move could be (in terms > > of distance from > > any previous move), so those would have to be represented (in any > > alphabet) by arbitrarily > > long finite strings.  Probably the easiest alphabet to use is one with > > 3 symbols -- 0,1, and a > > separation-symbol telling where the code for the previous move ends > > and the next move begins. > > > You could then define a relevant formal language as consisting of all > > and only those strings > > in which the angel gets trapped, but that would be too simplistic > > since there is no way of > > separating (within these) those in which the angel was actually trying > > to escape, > > from those in which suboptimal moving allowed the angel to be caught > > even though (with > > better choices) it could have escaped. > > > I don't even know if this is the direction you were intending to go, > > though, since you said > > "question".  That almost invites thinking of a first-order logical > > language as a formal > > language and doing it that way (since that version of "formal > > language") is one in which > > every statement is also a question, especially if it is not a theorem > > or the negation of a theorem.- Hide quoted text - > > - Show quoted text - |