Guys, can you help me finding the book? It was something about formal languages and grammars and automated theorem proving. I only remember a single passage from it. It tells about people developing computer reasoning system. They gave it an input like "The guy shaves himself with a razor each morning" and the system answered that it's a logical mistake, because razor is made of metal and a human can't have metal parts. It's not literal narrative just the summary of what I remembered.