В работе представлена возможность автоматизации сборки механизмов при помощи методов автоматического доказательства теорем. Процесс автоматизации в данной работе основан на применении метода представления и обработки знаний в типово-кванторном языке L позитивно-образованных формул (по-формул) с применением соответствующего первопорядкового логического исчисления J (с единственным правилом вывода ω), которое имеет ряд существенных преимуществ над другими методами. Представлен пример на основе известной задачи планирования BLOCKSWORLD с дополнительными ограничениями на совместимость блоков, что является формализацией задачи о допусках и посадках.